Metamath Proof Explorer


Theorem cdlemh2

Description: Part of proof of Lemma H of Crawley p. 118. (Contributed by NM, 16-Jun-2013)

Ref Expression
Hypotheses cdlemh.b B=BaseK
cdlemh.l ˙=K
cdlemh.j ˙=joinK
cdlemh.m ˙=meetK
cdlemh.a A=AtomsK
cdlemh.h H=LHypK
cdlemh.t T=LTrnKW
cdlemh.r R=trLKW
cdlemh.s S=P˙RG˙Q˙RGF-1
cdlemh.z 0˙=0.K
Assertion cdlemh2 KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGS˙W=0˙

Proof

Step Hyp Ref Expression
1 cdlemh.b B=BaseK
2 cdlemh.l ˙=K
3 cdlemh.j ˙=joinK
4 cdlemh.m ˙=meetK
5 cdlemh.a A=AtomsK
6 cdlemh.h H=LHypK
7 cdlemh.t T=LTrnKW
8 cdlemh.r R=trLKW
9 cdlemh.s S=P˙RG˙Q˙RGF-1
10 cdlemh.z 0˙=0.K
11 9 oveq1i S˙W=P˙RG˙Q˙RGF-1˙W
12 simp11l KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGKHL
13 hlol KHLKOL
14 12 13 syl KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGKOL
15 12 hllatd KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGKLat
16 simp2ll KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGPA
17 1 5 atbase PAPB
18 16 17 syl KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGPB
19 simp11r KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGWH
20 12 19 jca KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGKHLWH
21 simp13 KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGGT
22 1 6 7 8 trlcl KHLWHGTRGB
23 20 21 22 syl2anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGRGB
24 1 3 latjcl KLatPBRGBP˙RGB
25 15 18 23 24 syl3anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGP˙RGB
26 simp2rl KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGQA
27 1 5 atbase QAQB
28 26 27 syl KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGQB
29 simp12 KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGFT
30 6 7 ltrncnv KHLWHFTF-1T
31 20 29 30 syl2anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGF-1T
32 6 7 ltrnco KHLWHGTF-1TGF-1T
33 20 21 31 32 syl3anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGGF-1T
34 1 6 7 8 trlcl KHLWHGF-1TRGF-1B
35 20 33 34 syl2anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGRGF-1B
36 1 3 latjcl KLatQBRGF-1BQ˙RGF-1B
37 15 28 35 36 syl3anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGQ˙RGF-1B
38 1 6 lhpbase WHWB
39 19 38 syl KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGWB
40 1 4 latmassOLD KOLP˙RGBQ˙RGF-1BWBP˙RG˙Q˙RGF-1˙W=P˙RG˙Q˙RGF-1˙W
41 14 25 37 39 40 syl13anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGP˙RG˙Q˙RGF-1˙W=P˙RG˙Q˙RGF-1˙W
42 simp2r KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGQA¬Q˙W
43 2 4 10 5 6 lhpmat KHLWHQA¬Q˙WQ˙W=0˙
44 20 42 43 syl2anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGQ˙W=0˙
45 44 oveq1d KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGQ˙W˙RGF-1=0˙˙RGF-1
46 2 6 7 8 trlle KHLWHGF-1TRGF-1˙W
47 20 33 46 syl2anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGRGF-1˙W
48 1 2 3 4 5 atmod4i2 KHLQARGF-1BWBRGF-1˙WQ˙W˙RGF-1=Q˙RGF-1˙W
49 12 26 35 39 47 48 syl131anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGQ˙W˙RGF-1=Q˙RGF-1˙W
50 1 3 10 olj02 KOLRGF-1B0˙˙RGF-1=RGF-1
51 14 35 50 syl2anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRG0˙˙RGF-1=RGF-1
52 45 49 51 3eqtr3rd KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGRGF-1=Q˙RGF-1˙W
53 52 oveq2d KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGP˙RG˙RGF-1=P˙RG˙Q˙RGF-1˙W
54 simp2l KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGPA¬P˙W
55 21 31 jca KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGGTF-1T
56 simp33 KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGRFRG
57 56 necomd KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGRGRF
58 6 7 8 trlcnv KHLWHFTRF-1=RF
59 20 29 58 syl2anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGRF-1=RF
60 57 59 neeqtrrd KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGRGRF-1
61 simp31 KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGFIB
62 1 6 7 ltrncnvnid KHLWHFTFIBF-1IB
63 20 29 61 62 syl3anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGF-1IB
64 1 6 7 8 trlcone KHLWHGTF-1TRGRF-1F-1IBRGRGF-1
65 20 55 60 63 64 syl112anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGRGRGF-1
66 simp32 KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGGIB
67 1 5 6 7 8 trlnidat KHLWHGTGIBRGA
68 20 21 66 67 syl3anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGRGA
69 2 6 7 8 trlle KHLWHGTRG˙W
70 20 21 69 syl2anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGRG˙W
71 5 6 7 8 trlcoat KHLWHGTF-1TRGRF-1RGF-1A
72 20 55 60 71 syl3anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGRGF-1A
73 2 3 4 10 5 6 lhp2at0 KHLWHPA¬P˙WRGRGF-1RGARG˙WRGF-1ARGF-1˙WP˙RG˙RGF-1=0˙
74 20 54 65 68 70 72 47 73 syl322anc KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGP˙RG˙RGF-1=0˙
75 41 53 74 3eqtr2rd KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRG0˙=P˙RG˙Q˙RGF-1˙W
76 11 75 eqtr4id KHLWHFTGTPA¬P˙WQA¬Q˙WFIBGIBRFRGS˙W=0˙