Metamath Proof Explorer


Theorem cdlemk12

Description: Part of proof of Lemma K of Crawley p. 118. Eq. 4, line 10, p. 119. (Contributed by NM, 30-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.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
Assertion cdlemk12 K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X S G P = P ˙ G P ˙ S X P ˙ 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.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
10 simp11l K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X K HL
11 simp22l K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X P A
12 simp11 K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X K HL W H
13 simp13 K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X G T
14 2 4 5 6 ltrnat K HL W H G T P A G P A
15 12 13 11 14 syl3anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X G P A
16 simp12 K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X F T
17 simp21r K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X X T
18 12 16 17 3jca K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X K HL W H F T X T
19 simp21l K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X N T
20 simp22 K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X P A ¬ P ˙ W
21 simp23 K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R F = R N
22 19 20 21 3jca K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X N T P A ¬ P ˙ W R F = R N
23 simp311 K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X F I B
24 simp313 K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X X I B
25 simp32r K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R X R F
26 1 2 3 4 5 6 7 8 9 cdlemksat K HL W H F T X T N T P A ¬ P ˙ W R F = R N F I B X I B R X R F S X P A
27 18 22 23 24 25 26 syl113anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X S X P A
28 simp33 K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R G R X
29 28 necomd K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R X R G
30 4 5 6 7 trlcocnvat K HL W H X T G T R X R G R X G -1 A
31 12 17 13 29 30 syl121anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R X G -1 A
32 simp1 K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X K HL W H F T G T
33 simp312 K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X G I B
34 simp32l K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R G R F
35 1 2 3 4 5 6 7 8 9 cdlemksat K HL W H F T G T N T P A ¬ P ˙ W R F = R N F I B G I B R G R F S G P A
36 32 22 23 33 34 35 syl113anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X S G P A
37 1 2 3 4 5 6 7 8 9 cdlemksv2 K HL W H F T G T N T P A ¬ P ˙ W R F = R N F I B G I B R G R F S G P = P ˙ R G ˙ N P ˙ R G F -1
38 32 22 23 33 34 37 syl113anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X S G P = P ˙ R G ˙ N P ˙ R G F -1
39 10 hllatd K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X K Lat
40 1 4 5 6 7 trlnidat K HL W H G T G I B R G A
41 12 13 33 40 syl3anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R G A
42 1 3 4 hlatjcl K HL P A R G A P ˙ R G B
43 10 11 41 42 syl3anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X P ˙ R G B
44 2 4 5 6 ltrnat K HL W H N T P A N P A
45 12 19 11 44 syl3anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X N P A
46 4 5 6 7 trlcocnvat K HL W H G T F T R G R F R G F -1 A
47 12 13 16 34 46 syl121anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R G F -1 A
48 1 3 4 hlatjcl K HL N P A R G F -1 A N P ˙ R G F -1 B
49 10 45 47 48 syl3anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X N P ˙ R G F -1 B
50 1 2 8 latmle1 K Lat P ˙ R G B N P ˙ R G F -1 B P ˙ R G ˙ N P ˙ R G F -1 ˙ P ˙ R G
51 39 43 49 50 syl3anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X P ˙ R G ˙ N P ˙ R G F -1 ˙ P ˙ R G
52 38 51 eqbrtrd K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X S G P ˙ P ˙ R G
53 2 3 4 5 6 7 trljat1 K HL W H G T P A ¬ P ˙ W P ˙ R G = P ˙ G P
54 12 13 20 53 syl3anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X P ˙ R G = P ˙ G P
55 52 54 breqtrd K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X S G P ˙ P ˙ G P
56 simp2 K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X N T X T P A ¬ P ˙ W R F = R N
57 simp31 K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X F I B G I B X I B
58 eqid G P ˙ X P ˙ R G F -1 ˙ R X F -1 = G P ˙ X P ˙ R G F -1 ˙ R X F -1
59 1 2 3 4 5 6 7 8 9 58 cdlemk11 K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F S G P ˙ S X P ˙ R X G -1
60 32 56 57 34 25 59 syl113anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X S G P ˙ S X P ˙ R X G -1
61 2 3 4 hlatlej2 K HL P A R G A R G ˙ P ˙ R G
62 10 11 41 61 syl3anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R G ˙ P ˙ R G
63 62 54 breqtrd K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R G ˙ P ˙ G P
64 1 2 3 4 5 6 7 8 9 cdlemksel K HL W H F T X T N T P A ¬ P ˙ W R F = R N F I B X I B R X R F S X T
65 18 22 23 24 25 64 syl113anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X S X T
66 2 4 5 6 ltrnel K HL W H S X T P A ¬ P ˙ W S X P A ¬ S X P ˙ W
67 12 65 20 66 syl3anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X S X P A ¬ S X P ˙ W
68 5 6 ltrncnv K HL W H G T G -1 T
69 12 13 68 syl2anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X G -1 T
70 5 6 7 trlcnv K HL W H G T R G -1 = R G
71 12 13 70 syl2anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R G -1 = R G
72 71 28 eqnetrd K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R G -1 R X
73 1 5 6 7 trlcone K HL W H G -1 T X T R G -1 R X X I B R G -1 R G -1 X
74 12 69 17 72 24 73 syl122anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R G -1 R G -1 X
75 74 necomd K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R G -1 X R G -1
76 5 6 ltrncom K HL W H G -1 T X T G -1 X = X G -1
77 12 69 17 76 syl3anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X G -1 X = X G -1
78 77 fveq2d K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R G -1 X = R X G -1
79 75 78 71 3netr3d K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R X G -1 R G
80 5 6 ltrnco K HL W H X T G -1 T X G -1 T
81 12 17 69 80 syl3anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X X G -1 T
82 2 5 6 7 trlle K HL W H X G -1 T R X G -1 ˙ W
83 12 81 82 syl2anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R X G -1 ˙ W
84 2 5 6 7 trlle K HL W H G T R G ˙ W
85 12 13 84 syl2anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X R G ˙ W
86 2 3 4 5 lhp2atnle K HL W H S X P A ¬ S X P ˙ W R X G -1 R G R X G -1 A R X G -1 ˙ W R G A R G ˙ W ¬ R G ˙ S X P ˙ R X G -1
87 12 67 79 31 83 41 85 86 syl322anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X ¬ R G ˙ S X P ˙ R X G -1
88 nbrne1 R G ˙ P ˙ G P ¬ R G ˙ S X P ˙ R X G -1 P ˙ G P S X P ˙ R X G -1
89 63 87 88 syl2anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X P ˙ G P S X P ˙ R X G -1
90 2 3 8 4 2atm K HL P A G P A S X P A R X G -1 A S G P A S G P ˙ P ˙ G P S G P ˙ S X P ˙ R X G -1 P ˙ G P S X P ˙ R X G -1 S G P = P ˙ G P ˙ S X P ˙ R X G -1
91 10 11 15 27 31 36 55 60 89 90 syl333anc K HL W H F T G T N T X T P A ¬ P ˙ W R F = R N F I B G I B X I B R G R F R X R F R G R X S G P = P ˙ G P ˙ S X P ˙ R X G -1