Metamath Proof Explorer


Theorem cdlemk15

Description: Part of proof of Lemma K of Crawley p. 118. Line 21 on p. 119. O , D are k_1, f_1. (Contributed by NM, 1-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
Assertion cdlemk15 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F N P ˙ P ˙ R F ˙ O P ˙ R F D -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 simp11l K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F K HL
12 simp22l K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F P A
13 simp11 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F K HL W H
14 simp21 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F N T
15 2 5 6 7 ltrnat K HL W H N T P A N P A
16 13 14 12 15 syl3anc K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F N P A
17 2 3 5 hlatlej2 K HL P A N P A N P ˙ P ˙ N P
18 11 12 16 17 syl3anc K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F N P ˙ P ˙ N P
19 simp23 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F R F = R N
20 19 oveq2d K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F P ˙ R F = P ˙ R N
21 simp22 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F P A ¬ P ˙ W
22 2 3 5 6 7 8 trljat1 K HL W H N T P A ¬ P ˙ W P ˙ R N = P ˙ N P
23 13 14 21 22 syl3anc K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F P ˙ R N = P ˙ N P
24 20 23 eqtr2d K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F P ˙ N P = P ˙ R F
25 18 24 breqtrd K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F N P ˙ P ˙ R F
26 1 2 3 4 5 6 7 8 9 10 cdlemk14 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F N P ˙ O P ˙ R F D -1
27 11 hllatd K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F K Lat
28 1 5 atbase N P A N P B
29 16 28 syl K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F N P B
30 simp12 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F F T
31 simp31 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F F I B
32 1 5 6 7 8 trlnidat K HL W H F T F I B R F A
33 13 30 31 32 syl3anc K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F R F A
34 1 3 5 hlatjcl K HL P A R F A P ˙ R F B
35 11 12 33 34 syl3anc K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F P ˙ R F B
36 10 fveq1i O P = S D P
37 1 2 3 5 6 7 8 4 9 cdlemksat K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F S D P A
38 36 37 eqeltrid K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F O P A
39 simp13 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F D T
40 simp33 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F R D R F
41 40 necomd K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F R F R D
42 5 6 7 8 trlcocnvat K HL W H F T D T R F R D R F D -1 A
43 13 30 39 41 42 syl121anc K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F R F D -1 A
44 1 3 5 hlatjcl K HL O P A R F D -1 A O P ˙ R F D -1 B
45 11 38 43 44 syl3anc K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F O P ˙ R F D -1 B
46 1 2 4 latlem12 K Lat N P B P ˙ R F B O P ˙ R F D -1 B N P ˙ P ˙ R F N P ˙ O P ˙ R F D -1 N P ˙ P ˙ R F ˙ O P ˙ R F D -1
47 27 29 35 45 46 syl13anc K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F N P ˙ P ˙ R F N P ˙ O P ˙ R F D -1 N P ˙ P ˙ R F ˙ O P ˙ R F D -1
48 25 26 47 mpbi2and K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F N P ˙ P ˙ R F ˙ O P ˙ R F D -1