Metamath Proof Explorer


Theorem cdlemk10

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

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
cdlemk.v1 V = G P ˙ X P ˙ R G F -1 ˙ R X F -1
Assertion cdlemk10 K HL W H F T G T X T P A ¬ P ˙ W V ˙ R X G -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 cdlemk.v1 V = G P ˙ X P ˙ R G F -1 ˙ R X F -1
10 simp1 K HL W H F T G T X T P A ¬ P ˙ W K HL W H
11 simp22 K HL W H F T G T X T P A ¬ P ˙ W G T
12 simp21 K HL W H F T G T X T P A ¬ P ˙ W F T
13 5 6 ltrncnv K HL W H F T F -1 T
14 10 12 13 syl2anc K HL W H F T G T X T P A ¬ P ˙ W F -1 T
15 5 6 ltrnco K HL W H G T F -1 T G F -1 T
16 10 11 14 15 syl3anc K HL W H F T G T X T P A ¬ P ˙ W G F -1 T
17 2 5 6 7 trlle K HL W H G F -1 T R G F -1 ˙ W
18 10 16 17 syl2anc K HL W H F T G T X T P A ¬ P ˙ W R G F -1 ˙ W
19 simp23 K HL W H F T G T X T P A ¬ P ˙ W X T
20 5 6 ltrnco K HL W H X T F -1 T X F -1 T
21 10 19 14 20 syl3anc K HL W H F T G T X T P A ¬ P ˙ W X F -1 T
22 2 5 6 7 trlle K HL W H X F -1 T R X F -1 ˙ W
23 10 21 22 syl2anc K HL W H F T G T X T P A ¬ P ˙ W R X F -1 ˙ W
24 simp1l K HL W H F T G T X T P A ¬ P ˙ W K HL
25 24 hllatd K HL W H F T G T X T P A ¬ P ˙ W K Lat
26 1 5 6 7 trlcl K HL W H G F -1 T R G F -1 B
27 10 16 26 syl2anc K HL W H F T G T X T P A ¬ P ˙ W R G F -1 B
28 1 5 6 7 trlcl K HL W H X F -1 T R X F -1 B
29 10 21 28 syl2anc K HL W H F T G T X T P A ¬ P ˙ W R X F -1 B
30 simp1r K HL W H F T 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 F T G T X T P A ¬ P ˙ W W B
33 1 2 3 latjle12 K Lat R G F -1 B R X F -1 B W B R G F -1 ˙ W R X F -1 ˙ W R G F -1 ˙ R X F -1 ˙ W
34 25 27 29 32 33 syl13anc K HL W H F T G T X T P A ¬ P ˙ W R G F -1 ˙ W R X F -1 ˙ W R G F -1 ˙ R X F -1 ˙ W
35 18 23 34 mpbi2and K HL W H F T G T X T P A ¬ P ˙ W R G F -1 ˙ R X F -1 ˙ W
36 1 3 latjcl K Lat R G F -1 B R X F -1 B R G F -1 ˙ R X F -1 B
37 25 27 29 36 syl3anc K HL W H F T G T X T P A ¬ P ˙ W R G F -1 ˙ R X F -1 B
38 simp3l K HL W H F T G T X T P A ¬ P ˙ W P A
39 2 4 5 6 ltrnat K HL W H G T P A G P A
40 10 11 38 39 syl3anc K HL W H F T G T X T P A ¬ P ˙ W G P A
41 2 4 5 6 ltrnat K HL W H X T P A X P A
42 10 19 38 41 syl3anc K HL W H F T G T X T P A ¬ P ˙ W X P A
43 1 3 4 hlatjcl K HL G P A X P A G P ˙ X P B
44 24 40 42 43 syl3anc K HL W H F T G T X T P A ¬ P ˙ W G P ˙ X P B
45 1 2 8 latmlem2 K Lat R G F -1 ˙ R X F -1 B W B G P ˙ X P B R G F -1 ˙ R X F -1 ˙ W G P ˙ X P ˙ R G F -1 ˙ R X F -1 ˙ G P ˙ X P ˙ W
46 25 37 32 44 45 syl13anc K HL W H F T G T X T P A ¬ P ˙ W R G F -1 ˙ R X F -1 ˙ W G P ˙ X P ˙ R G F -1 ˙ R X F -1 ˙ G P ˙ X P ˙ W
47 35 46 mpd K HL W H F T G T X T P A ¬ P ˙ W G P ˙ X P ˙ R G F -1 ˙ R X F -1 ˙ G P ˙ X P ˙ W
48 simp3 K HL W H F T G T X T P A ¬ P ˙ W P A ¬ P ˙ W
49 1 2 3 4 5 6 7 8 cdlemk9 K HL W H G T X T P A ¬ P ˙ W G P ˙ X P ˙ W = R X G -1
50 24 30 11 19 48 49 syl221anc K HL W H F T G T X T P A ¬ P ˙ W G P ˙ X P ˙ W = R X G -1
51 47 50 breqtrd K HL W H F T G T X T P A ¬ P ˙ W G P ˙ X P ˙ R G F -1 ˙ R X F -1 ˙ R X G -1
52 9 51 eqbrtrid K HL W H F T G T X T P A ¬ P ˙ W V ˙ R X G -1