Metamath Proof Explorer


Theorem cdlemk11u

Description: Part of proof of Lemma K of Crawley p. 118. Line 17, p. 119, showing Eq. 3 (line 8, p. 119) for the sigma_1 ( U ) case. (Contributed by NM, 4-Jul-2013)

Ref Expression
Hypotheses cdlemk1.b B = Base K
cdlemk1.l ˙ = K
cdlemk1.j ˙ = join K
cdlemk1.m ˙ = meet K
cdlemk1.a A = Atoms K
cdlemk1.h H = LHyp K
cdlemk1.t T = LTrn K W
cdlemk1.r R = trL K W
cdlemk1.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
cdlemk1.o O = S D
cdlemk1.u U = e T ι j T | j P = P ˙ R e ˙ O P ˙ R e D -1
cdlemk1.v V = G P ˙ X P ˙ R G D -1 ˙ R X D -1
Assertion cdlemk11u K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D U G P ˙ U X P ˙ R X G -1

Proof

Step Hyp Ref Expression
1 cdlemk1.b B = Base K
2 cdlemk1.l ˙ = K
3 cdlemk1.j ˙ = join K
4 cdlemk1.m ˙ = meet K
5 cdlemk1.a A = Atoms K
6 cdlemk1.h H = LHyp K
7 cdlemk1.t T = LTrn K W
8 cdlemk1.r R = trL K W
9 cdlemk1.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
10 cdlemk1.o O = S D
11 cdlemk1.u U = e T ι j T | j P = P ˙ R e ˙ O P ˙ R e D -1
12 cdlemk1.v V = G P ˙ X P ˙ R G D -1 ˙ R X D -1
13 simp11l K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D K HL
14 13 hllatd K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D K Lat
15 simp11r K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D W H
16 13 15 jca K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D K HL W H
17 simp23 K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D R F = R N
18 simp212 K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D G T
19 simp12 K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D F T
20 simp13 K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D D T
21 simp211 K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D N T
22 simp331 K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D R D R F
23 simp332 K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D R G R D
24 23 necomd K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D R D R G
25 22 24 jca K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D R D R F R D R G
26 simp311 K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D F I B
27 simp313 K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D G I B
28 simp312 K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D D I B
29 26 27 28 3jca K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D F I B G I B D I B
30 simp22 K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D P A ¬ P ˙ W
31 1 2 3 4 5 6 7 8 9 10 11 cdlemkuat K HL W H R F = R N G T F T D T N T R D R F R D R G F I B G I B D I B P A ¬ P ˙ W U G P A
32 16 17 18 19 20 21 25 29 30 31 syl333anc K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D U G P A
33 1 5 atbase U G P A U G P B
34 32 33 syl K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D U G P B
35 simp213 K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D X T
36 simp333 K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D R X R D
37 36 necomd K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D R D R X
38 22 37 jca K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D R D R F R D R X
39 simp32 K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D X I B
40 26 39 28 3jca K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D F I B X I B D I B
41 1 2 3 4 5 6 7 8 9 10 11 cdlemkuat K HL W H R F = R N X T F T D T N T R D R F R D R X F I B X I B D I B P A ¬ P ˙ W U X P A
42 16 17 35 19 20 21 38 40 30 41 syl333anc K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D U X P A
43 1 5 atbase U X P A U X P B
44 42 43 syl K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D U X P B
45 simp22l K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D P A
46 1 2 3 5 6 7 8 4 12 cdlemkvcl K HL W H D T G T X T P A V B
47 13 15 20 18 35 45 46 syl231anc K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D V B
48 1 3 latjcl K Lat U X P B V B U X P ˙ V B
49 14 44 47 48 syl3anc K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D U X P ˙ V B
50 6 7 ltrncnv K HL W H G T G -1 T
51 16 18 50 syl2anc K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D G -1 T
52 6 7 ltrnco K HL W H X T G -1 T X G -1 T
53 16 35 51 52 syl3anc K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D X G -1 T
54 1 6 7 8 trlcl K HL W H X G -1 T R X G -1 B
55 16 53 54 syl2anc K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D R X G -1 B
56 1 3 latjcl K Lat U X P B R X G -1 B U X P ˙ R X G -1 B
57 14 44 55 56 syl3anc K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D U X P ˙ R X G -1 B
58 1 2 3 4 5 6 7 8 9 10 11 12 cdlemk7u K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D U G P ˙ U X P ˙ V
59 1 2 3 5 6 7 8 4 12 cdlemk10 K HL W H D T G T X T P A ¬ P ˙ W V ˙ R X G -1
60 13 15 20 18 35 30 59 syl231anc K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D V ˙ R X G -1
61 1 2 3 latjlej2 K Lat V B R X G -1 B U X P B V ˙ R X G -1 U X P ˙ V ˙ U X P ˙ R X G -1
62 14 47 55 44 61 syl13anc K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D V ˙ R X G -1 U X P ˙ V ˙ U X P ˙ R X G -1
63 60 62 mpd K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D U X P ˙ V ˙ U X P ˙ R X G -1
64 1 2 14 34 49 57 58 63 lattrd K HL W H F T D T N T G T X T P A ¬ P ˙ W R F = R N F I B D I B G I B X I B R D R F R G R D R X R D U G P ˙ U X P ˙ R X G -1