Metamath Proof Explorer


Theorem cdlemi

Description: Lemma I of Crawley p. 118. (Contributed by NM, 19-Jun-2013)

Ref Expression
Hypotheses cdlemi.b B = Base K
cdlemi.l ˙ = K
cdlemi.j ˙ = join K
cdlemi.m ˙ = meet K
cdlemi.a A = Atoms K
cdlemi.h H = LHyp K
cdlemi.t T = LTrn K W
cdlemi.r R = trL K W
cdlemi.e E = TEndo K W
cdlemi.s S = P ˙ R G ˙ U F P ˙ R G F -1
Assertion cdlemi K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U G P = S

Proof

Step Hyp Ref Expression
1 cdlemi.b B = Base K
2 cdlemi.l ˙ = K
3 cdlemi.j ˙ = join K
4 cdlemi.m ˙ = meet K
5 cdlemi.a A = Atoms K
6 cdlemi.h H = LHyp K
7 cdlemi.t T = LTrn K W
8 cdlemi.r R = trL K W
9 cdlemi.e E = TEndo K W
10 cdlemi.s S = P ˙ R G ˙ U F P ˙ R G F -1
11 simp11l K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G K HL
12 simp11r K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G W H
13 simp2l K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U E
14 simp13 K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G G T
15 simp2r K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G P A ¬ P ˙ W
16 1 2 3 4 5 6 7 8 9 cdlemi1 K HL W H U E G T P A ¬ P ˙ W U G P ˙ P ˙ R G
17 11 12 13 14 15 16 syl221anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U G P ˙ P ˙ R G
18 simp12 K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G F T
19 1 2 3 4 5 6 7 8 9 cdlemi2 K HL W H U E F T G T P A ¬ P ˙ W U G P ˙ U F P ˙ R G F -1
20 11 12 13 18 14 15 19 syl231anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U G P ˙ U F P ˙ R G F -1
21 11 hllatd K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G K Lat
22 simp11 K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G K HL W H
23 6 7 9 tendocl K HL W H U E G T U G T
24 22 13 14 23 syl3anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U G T
25 simp2rl K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G P A
26 1 5 atbase P A P B
27 25 26 syl K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G P B
28 1 6 7 ltrncl K HL W H U G T P B U G P B
29 22 24 27 28 syl3anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U G P B
30 1 6 7 8 trlcl K HL W H G T R G B
31 22 14 30 syl2anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G R G B
32 1 3 latjcl K Lat P B R G B P ˙ R G B
33 21 27 31 32 syl3anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G P ˙ R G B
34 6 7 9 tendocl K HL W H U E F T U F T
35 22 13 18 34 syl3anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U F T
36 1 6 7 ltrncl K HL W H U F T P B U F P B
37 22 35 27 36 syl3anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U F P B
38 6 7 ltrncnv K HL W H F T F -1 T
39 22 18 38 syl2anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G F -1 T
40 6 7 ltrnco K HL W H G T F -1 T G F -1 T
41 22 14 39 40 syl3anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G G F -1 T
42 1 6 7 8 trlcl K HL W H G F -1 T R G F -1 B
43 22 41 42 syl2anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G R G F -1 B
44 1 3 latjcl K Lat U F P B R G F -1 B U F P ˙ R G F -1 B
45 21 37 43 44 syl3anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U F P ˙ R G F -1 B
46 1 2 4 latlem12 K Lat U G P B P ˙ R G B U F P ˙ R G F -1 B U G P ˙ P ˙ R G U G P ˙ U F P ˙ R G F -1 U G P ˙ P ˙ R G ˙ U F P ˙ R G F -1
47 21 29 33 45 46 syl13anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U G P ˙ P ˙ R G U G P ˙ U F P ˙ R G F -1 U G P ˙ P ˙ R G ˙ U F P ˙ R G F -1
48 17 20 47 mpbi2and K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U G P ˙ P ˙ R G ˙ U F P ˙ R G F -1
49 hlatl K HL K AtLat
50 11 49 syl K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G K AtLat
51 2 5 6 7 ltrnat K HL W H U G T P A U G P A
52 22 24 25 51 syl3anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U G P A
53 2 5 6 7 ltrnel K HL W H U F T P A ¬ P ˙ W U F P A ¬ U F P ˙ W
54 22 35 15 53 syl3anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U F P A ¬ U F P ˙ W
55 1 2 3 4 5 6 7 8 9 cdlemi1 K HL W H U E F T P A ¬ P ˙ W U F P ˙ P ˙ R F
56 11 12 13 18 15 55 syl221anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U F P ˙ P ˙ R F
57 15 54 56 3jca K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G P A ¬ P ˙ W U F P A ¬ U F P ˙ W U F P ˙ P ˙ R F
58 eqid P ˙ R G ˙ U F P ˙ R G F -1 = P ˙ R G ˙ U F P ˙ R G F -1
59 1 2 3 4 5 6 7 8 58 cdlemh K HL W H F T G T P A ¬ P ˙ W U F P A ¬ U F P ˙ W U F P ˙ P ˙ R F F I B G I B R F R G P ˙ R G ˙ U F P ˙ R G F -1 A ¬ P ˙ R G ˙ U F P ˙ R G F -1 ˙ W
60 59 simpld K HL W H F T G T P A ¬ P ˙ W U F P A ¬ U F P ˙ W U F P ˙ P ˙ R F F I B G I B R F R G P ˙ R G ˙ U F P ˙ R G F -1 A
61 57 60 syld3an2 K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G P ˙ R G ˙ U F P ˙ R G F -1 A
62 2 5 atcmp K AtLat U G P A P ˙ R G ˙ U F P ˙ R G F -1 A U G P ˙ P ˙ R G ˙ U F P ˙ R G F -1 U G P = P ˙ R G ˙ U F P ˙ R G F -1
63 50 52 61 62 syl3anc K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U G P ˙ P ˙ R G ˙ U F P ˙ R G F -1 U G P = P ˙ R G ˙ U F P ˙ R G F -1
64 48 63 mpbid K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U G P = P ˙ R G ˙ U F P ˙ R G F -1
65 64 10 syl6eqr K HL W H F T G T U E P A ¬ P ˙ W F I B G I B R F R G U G P = S