Metamath Proof Explorer


Theorem cdlemk9bN

Description: Part of proof of Lemma K of Crawley p. 118. TODO: is this needed? If so, shorten with cdlemk9 if that one is also needed. (Contributed by NM, 28-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemk.b B=BaseK
cdlemk.l ˙=K
cdlemk.j ˙=joinK
cdlemk.a A=AtomsK
cdlemk.h H=LHypK
cdlemk.t T=LTrnKW
cdlemk.r R=trLKW
cdlemk.m ˙=meetK
Assertion cdlemk9bN KHLWHGTXTPA¬P˙WGP˙XP˙W=RGX-1

Proof

Step Hyp Ref Expression
1 cdlemk.b B=BaseK
2 cdlemk.l ˙=K
3 cdlemk.j ˙=joinK
4 cdlemk.a A=AtomsK
5 cdlemk.h H=LHypK
6 cdlemk.t T=LTrnKW
7 cdlemk.r R=trLKW
8 cdlemk.m ˙=meetK
9 1 2 3 4 5 6 7 8 cdlemk8 KHLWHGTXTPA¬P˙WGP˙XP=GP˙RXG-1
10 9 oveq1d KHLWHGTXTPA¬P˙WGP˙XP˙W=GP˙RXG-1˙W
11 simp1 KHLWHGTXTPA¬P˙WKHLWH
12 2 4 5 6 ltrnel KHLWHGTPA¬P˙WGPA¬GP˙W
13 12 3adant2r KHLWHGTXTPA¬P˙WGPA¬GP˙W
14 eqid 0.K=0.K
15 2 8 14 4 5 lhpmat KHLWHGPA¬GP˙WGP˙W=0.K
16 11 13 15 syl2anc KHLWHGTXTPA¬P˙WGP˙W=0.K
17 16 oveq1d KHLWHGTXTPA¬P˙WGP˙W˙RXG-1=0.K˙RXG-1
18 simp1l KHLWHGTXTPA¬P˙WKHL
19 simp2l KHLWHGTXTPA¬P˙WGT
20 simp3l KHLWHGTXTPA¬P˙WPA
21 2 4 5 6 ltrnat KHLWHGTPAGPA
22 11 19 20 21 syl3anc KHLWHGTXTPA¬P˙WGPA
23 simp2r KHLWHGTXTPA¬P˙WXT
24 5 6 ltrncnv KHLWHGTG-1T
25 11 19 24 syl2anc KHLWHGTXTPA¬P˙WG-1T
26 5 6 ltrnco KHLWHXTG-1TXG-1T
27 11 23 25 26 syl3anc KHLWHGTXTPA¬P˙WXG-1T
28 1 5 6 7 trlcl KHLWHXG-1TRXG-1B
29 11 27 28 syl2anc KHLWHGTXTPA¬P˙WRXG-1B
30 simp1r KHLWHGTXTPA¬P˙WWH
31 1 5 lhpbase WHWB
32 30 31 syl KHLWHGTXTPA¬P˙WWB
33 2 5 6 7 trlle KHLWHXG-1TRXG-1˙W
34 11 27 33 syl2anc KHLWHGTXTPA¬P˙WRXG-1˙W
35 1 2 3 8 4 atmod4i2 KHLGPARXG-1BWBRXG-1˙WGP˙W˙RXG-1=GP˙RXG-1˙W
36 18 22 29 32 34 35 syl131anc KHLWHGTXTPA¬P˙WGP˙W˙RXG-1=GP˙RXG-1˙W
37 hlol KHLKOL
38 18 37 syl KHLWHGTXTPA¬P˙WKOL
39 1 3 14 olj02 KOLRXG-1B0.K˙RXG-1=RXG-1
40 38 29 39 syl2anc KHLWHGTXTPA¬P˙W0.K˙RXG-1=RXG-1
41 5 6 7 trlcocnv KHLWHGTXTRGX-1=RXG-1
42 11 19 23 41 syl3anc KHLWHGTXTPA¬P˙WRGX-1=RXG-1
43 40 42 eqtr4d KHLWHGTXTPA¬P˙W0.K˙RXG-1=RGX-1
44 17 36 43 3eqtr3d KHLWHGTXTPA¬P˙WGP˙RXG-1˙W=RGX-1
45 10 44 eqtrd KHLWHGTXTPA¬P˙WGP˙XP˙W=RGX-1