Metamath Proof Explorer


Theorem cdlemk52

Description: Part of proof of Lemma K of Crawley p. 118. Line 6, p. 120. G , I stand for g, h. X represents tau. (Contributed by NM, 23-Jul-2013)

Ref Expression
Hypotheses cdlemk5.b B=BaseK
cdlemk5.l ˙=K
cdlemk5.j ˙=joinK
cdlemk5.m ˙=meetK
cdlemk5.a A=AtomsK
cdlemk5.h H=LHypK
cdlemk5.t T=LTrnKW
cdlemk5.r R=trLKW
cdlemk5.z Z=P˙Rb˙NP˙RbF-1
cdlemk5.y Y=P˙Rg˙Z˙Rgb-1
cdlemk5.x X=ιzT|bTbIBRbRFRbRgzP=Y
Assertion cdlemk52 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXI/gXP=GI/gXP

Proof

Step Hyp Ref Expression
1 cdlemk5.b B=BaseK
2 cdlemk5.l ˙=K
3 cdlemk5.j ˙=joinK
4 cdlemk5.m ˙=meetK
5 cdlemk5.a A=AtomsK
6 cdlemk5.h H=LHypK
7 cdlemk5.t T=LTrnKW
8 cdlemk5.r R=trLKW
9 cdlemk5.z Z=P˙Rb˙NP˙RbF-1
10 cdlemk5.y Y=P˙Rg˙Z˙Rgb-1
11 cdlemk5.x X=ιzT|bTbIBRbRFRbRgzP=Y
12 simp11l KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIKHL
13 12 hllatd KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIKLat
14 simp11 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIKHLWH
15 simp12 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIFTFIB
16 simp13 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIGTGIB
17 simp21 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRINT
18 simp22 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIPA¬P˙W
19 simp23 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIRF=RN
20 1 2 3 4 5 6 7 8 9 10 11 cdlemk35s KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNG/gXT
21 14 15 16 17 18 19 20 syl132anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXT
22 simp31 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIIT
23 simp32 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIIIB
24 22 23 jca KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIITIIB
25 1 2 3 4 5 6 7 8 9 10 11 cdlemk35s KHLWHFTFIBITIIBNTPA¬P˙WRF=RNI/gXT
26 14 15 24 17 18 19 25 syl132anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRII/gXT
27 6 7 ltrnco KHLWHG/gXTI/gXTG/gXI/gXT
28 14 21 26 27 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXI/gXT
29 simp22l KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIPA
30 2 5 6 7 ltrnat KHLWHG/gXI/gXTPAG/gXI/gXPA
31 14 28 29 30 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXI/gXPA
32 1 5 atbase G/gXI/gXPAG/gXI/gXPB
33 31 32 syl KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXI/gXPB
34 2 5 6 7 ltrnat KHLWHG/gXTPAG/gXPA
35 14 21 29 34 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXPA
36 1 5 atbase G/gXPAG/gXPB
37 35 36 syl KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXPB
38 1 6 7 8 trlcl KHLWHI/gXTRI/gXB
39 14 26 38 syl2anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIRI/gXB
40 1 3 latjcl KLatG/gXPBRI/gXBG/gXP˙RI/gXB
41 13 37 39 40 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXP˙RI/gXB
42 2 5 6 7 ltrnat KHLWHI/gXTPAI/gXPA
43 14 26 29 42 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRII/gXPA
44 1 5 atbase I/gXPAI/gXPB
45 43 44 syl KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRII/gXPB
46 1 6 7 8 trlcl KHLWHG/gXTRG/gXB
47 14 21 46 syl2anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIRG/gXB
48 1 3 latjcl KLatI/gXPBRG/gXBI/gXP˙RG/gXB
49 13 45 47 48 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRII/gXP˙RG/gXB
50 1 4 latmcl KLatG/gXP˙RI/gXBI/gXP˙RG/gXBG/gXP˙RI/gX˙I/gXP˙RG/gXB
51 13 41 49 50 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXP˙RI/gX˙I/gXP˙RG/gXB
52 simp11r KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIWH
53 1 5 6 7 8 trlnidat KHLWHITIIBRIA
54 12 52 22 23 53 syl211anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIRIA
55 1 3 5 hlatjcl KHLG/gXPARIAG/gXP˙RIB
56 12 35 54 55 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXP˙RIB
57 simp13l KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIGT
58 simp13r KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIGIB
59 1 5 6 7 8 trlnidat KHLWHGTGIBRGA
60 12 52 57 58 59 syl211anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIRGA
61 1 3 5 hlatjcl KHLI/gXPARGAI/gXP˙RGB
62 12 43 60 61 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRII/gXP˙RGB
63 1 4 latmcl KLatG/gXP˙RIBI/gXP˙RGBG/gXP˙RI˙I/gXP˙RGB
64 13 56 62 63 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXP˙RI˙I/gXP˙RGB
65 1 2 3 4 5 6 7 8 9 10 11 cdlemk50 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBG/gXI/gXP˙G/gXP˙RI/gX˙I/gXP˙RG/gX
66 24 65 syld3an3 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXI/gXP˙G/gXP˙RI/gX˙I/gXP˙RG/gX
67 1 2 3 4 5 6 7 8 9 10 11 cdlemk51 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBG/gXP˙RI/gX˙I/gXP˙RG/gX˙G/gXP˙RI˙I/gXP˙RG
68 24 67 syld3an3 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXP˙RI/gX˙I/gXP˙RG/gX˙G/gXP˙RI˙I/gXP˙RG
69 1 2 13 33 51 64 66 68 lattrd KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXI/gXP˙G/gXP˙RI˙I/gXP˙RG
70 1 2 3 4 5 6 7 8 9 10 11 cdlemk47 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIGI/gXP=G/gXP˙RI˙I/gXP˙RG
71 69 70 breqtrrd KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXI/gXP˙GI/gXP
72 hlatl KHLKAtLat
73 12 72 syl KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIKAtLat
74 6 7 ltrnco KHLWHGTITGIT
75 14 57 22 74 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIGIT
76 57 22 jca KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIGTIT
77 simp33 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIRGRI
78 1 6 7 8 trlconid KHLWHGTITRGRIGIIB
79 14 76 77 78 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIGIIB
80 75 79 jca KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIGITGIIB
81 1 2 3 4 5 6 7 8 9 10 11 cdlemk35s KHLWHFTFIBGITGIIBNTPA¬P˙WRF=RNGI/gXT
82 14 15 80 17 18 19 81 syl132anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIGI/gXT
83 2 5 6 7 ltrnat KHLWHGI/gXTPAGI/gXPA
84 14 82 29 83 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIGI/gXPA
85 2 5 atcmp KAtLatG/gXI/gXPAGI/gXPAG/gXI/gXP˙GI/gXPG/gXI/gXP=GI/gXP
86 73 31 84 85 syl3anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXI/gXP˙GI/gXPG/gXI/gXP=GI/gXP
87 71 86 mpbid KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNITIIBRGRIG/gXI/gXP=GI/gXP