Metamath Proof Explorer


Theorem cdlemeg46vrg

Description: TODO FIX COMMENT v_1 <_ r \/ g(s) p. 116 3rd line. (Contributed by NM, 3-Apr-2013)

Ref Expression
Hypotheses cdlemef46g.b B=BaseK
cdlemef46g.l ˙=K
cdlemef46g.j ˙=joinK
cdlemef46g.m ˙=meetK
cdlemef46g.a A=AtomsK
cdlemef46g.h H=LHypK
cdlemef46g.u U=P˙Q˙W
cdlemef46g.d D=t˙U˙Q˙P˙t˙W
cdlemefs46g.e E=P˙Q˙D˙s˙t˙W
cdlemef46g.f F=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
cdlemef46.v V=Q˙P˙W
cdlemef46.n N=v˙V˙P˙Q˙v˙W
cdlemefs46.o O=Q˙P˙N˙u˙v˙W
cdlemef46.g G=aBifQP¬a˙WιcB|uA¬u˙Wu˙a˙W=ac=ifu˙Q˙PιbB|vA¬v˙W¬v˙Q˙Pb=Ou/vN˙a˙Wa
cdlemeg46.y Y=R˙GS˙W
cdlemeg46.x X=FR˙S˙W
Assertion cdlemeg46vrg KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QX˙R˙GS

Proof

Step Hyp Ref Expression
1 cdlemef46g.b B=BaseK
2 cdlemef46g.l ˙=K
3 cdlemef46g.j ˙=joinK
4 cdlemef46g.m ˙=meetK
5 cdlemef46g.a A=AtomsK
6 cdlemef46g.h H=LHypK
7 cdlemef46g.u U=P˙Q˙W
8 cdlemef46g.d D=t˙U˙Q˙P˙t˙W
9 cdlemefs46g.e E=P˙Q˙D˙s˙t˙W
10 cdlemef46g.f F=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
11 cdlemef46.v V=Q˙P˙W
12 cdlemef46.n N=v˙V˙P˙Q˙v˙W
13 cdlemefs46.o O=Q˙P˙N˙u˙v˙W
14 cdlemef46.g G=aBifQP¬a˙WιcB|uA¬u˙Wu˙a˙W=ac=ifu˙Q˙PιbB|vA¬v˙W¬v˙Q˙Pb=Ou/vN˙a˙Wa
15 cdlemeg46.y Y=R˙GS˙W
16 cdlemeg46.x X=FR˙S˙W
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 cdlemeg46v1v2 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QX=Y
18 17 15 eqtrdi KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QX=R˙GS˙W
19 simp11l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QKHL
20 19 hllatd KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QKLat
21 simp22l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QRA
22 simp1 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QKHLWHPA¬P˙WQA¬Q˙W
23 simp23 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QSA¬S˙W
24 simp21 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QPQ
25 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdlemeg46fvaw KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQGSA¬GS˙W
26 25 simpld KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQGSA
27 22 23 24 26 syl3anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QGSA
28 1 3 5 hlatjcl KHLRAGSAR˙GSB
29 19 21 27 28 syl3anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QR˙GSB
30 simp11r KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QWH
31 1 6 lhpbase WHWB
32 30 31 syl KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QWB
33 1 2 4 latmle1 KLatR˙GSBWBR˙GS˙W˙R˙GS
34 20 29 32 33 syl3anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QR˙GS˙W˙R˙GS
35 18 34 eqbrtrd KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙WR˙P˙Q¬S˙P˙QX˙R˙GS