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 = Base K
cdlemk.l ˙ = K
cdlemk.j ˙ = join K
cdlemk.a A = Atoms K
cdlemk.h H = LHyp K
cdlemk.t T = LTrn K W
cdlemk.r R = trL K W
cdlemk.m ˙ = meet K
Assertion cdlemk9bN K HL W H G T X T P A ¬ P ˙ W G P ˙ X P ˙ W = R G X -1

Proof

Step Hyp Ref Expression
1 cdlemk.b B = Base K
2 cdlemk.l ˙ = K
3 cdlemk.j ˙ = join K
4 cdlemk.a A = Atoms K
5 cdlemk.h H = LHyp K
6 cdlemk.t T = LTrn K W
7 cdlemk.r R = trL K W
8 cdlemk.m ˙ = meet K
9 1 2 3 4 5 6 7 8 cdlemk8 K HL W H G T X T P A ¬ P ˙ W G P ˙ X P = G P ˙ R X G -1
10 9 oveq1d K HL W H G T X T P A ¬ P ˙ W G P ˙ X P ˙ W = G P ˙ R X G -1 ˙ W
11 simp1 K HL W H G T X T P A ¬ P ˙ W K HL W H
12 2 4 5 6 ltrnel K HL W H G T P A ¬ P ˙ W G P A ¬ G P ˙ W
13 12 3adant2r K HL W H G T X T P A ¬ P ˙ W G P A ¬ G P ˙ W
14 eqid 0. K = 0. K
15 2 8 14 4 5 lhpmat K HL W H G P A ¬ G P ˙ W G P ˙ W = 0. K
16 11 13 15 syl2anc K HL W H G T X T P A ¬ P ˙ W G P ˙ W = 0. K
17 16 oveq1d K HL W H G T X T P A ¬ P ˙ W G P ˙ W ˙ R X G -1 = 0. K ˙ R X G -1
18 simp1l K HL W H G T X T P A ¬ P ˙ W K HL
19 simp2l K HL W H G T X T P A ¬ P ˙ W G T
20 simp3l K HL W H G T X T P A ¬ P ˙ W P A
21 2 4 5 6 ltrnat K HL W H G T P A G P A
22 11 19 20 21 syl3anc K HL W H G T X T P A ¬ P ˙ W G P A
23 simp2r K HL W H G T X T P A ¬ P ˙ W X T
24 5 6 ltrncnv K HL W H G T G -1 T
25 11 19 24 syl2anc K HL W H G T X T P A ¬ P ˙ W G -1 T
26 5 6 ltrnco K HL W H X T G -1 T X G -1 T
27 11 23 25 26 syl3anc K HL W H G T X T P A ¬ P ˙ W X G -1 T
28 1 5 6 7 trlcl K HL W H X G -1 T R X G -1 B
29 11 27 28 syl2anc K HL W H G T X T P A ¬ P ˙ W R X G -1 B
30 simp1r K HL W H G T X T P A ¬ P ˙ W W H
31 1 5 lhpbase W H W B
32 30 31 syl K HL W H G T X T P A ¬ P ˙ W W B
33 2 5 6 7 trlle K HL W H X G -1 T R X G -1 ˙ W
34 11 27 33 syl2anc K HL W H G T X T P A ¬ P ˙ W R X G -1 ˙ W
35 1 2 3 8 4 atmod4i2 K HL G P A R X G -1 B W B R X G -1 ˙ W G P ˙ W ˙ R X G -1 = G P ˙ R X G -1 ˙ W
36 18 22 29 32 34 35 syl131anc K HL W H G T X T P A ¬ P ˙ W G P ˙ W ˙ R X G -1 = G P ˙ R X G -1 ˙ W
37 hlol K HL K OL
38 18 37 syl K HL W H G T X T P A ¬ P ˙ W K OL
39 1 3 14 olj02 K OL R X G -1 B 0. K ˙ R X G -1 = R X G -1
40 38 29 39 syl2anc K HL W H G T X T P A ¬ P ˙ W 0. K ˙ R X G -1 = R X G -1
41 5 6 7 trlcocnv K HL W H G T X T R G X -1 = R X G -1
42 11 19 23 41 syl3anc K HL W H G T X T P A ¬ P ˙ W R G X -1 = R X G -1
43 40 42 eqtr4d K HL W H G T X T P A ¬ P ˙ W 0. K ˙ R X G -1 = R G X -1
44 17 36 43 3eqtr3d K HL W H G T X T P A ¬ P ˙ W G P ˙ R X G -1 ˙ W = R G X -1
45 10 44 eqtrd K HL W H G T X T P A ¬ P ˙ W G P ˙ X P ˙ W = R G X -1