Metamath Proof Explorer


Theorem cdlemk14

Description: Part of proof of Lemma K of Crawley p. 118. Line 19 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 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

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 1 2 3 4 5 6 7 8 9 10 cdlemk13 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 = P ˙ R D ˙ N P ˙ R D F -1
12 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
13 12 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
14 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
15 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
16 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
17 simp32 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 I B
18 1 5 6 7 8 trlnidat K HL W H D T D I B R D A
19 15 16 17 18 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 D A
20 1 3 5 hlatjcl K HL P A R D A P ˙ R D B
21 12 14 19 20 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 D B
22 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
23 2 5 6 7 ltrnat K HL W H N T P A N P A
24 15 22 14 23 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
25 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
26 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
27 5 6 7 8 trlcocnvat K HL W H D T F T R D R F R D F -1 A
28 15 16 25 26 27 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 D F -1 A
29 1 3 5 hlatjcl K HL N P A R D F -1 A N P ˙ R D F -1 B
30 12 24 28 29 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 ˙ R D F -1 B
31 1 2 4 latmle2 K Lat P ˙ R D B N P ˙ R D F -1 B P ˙ R D ˙ N P ˙ R D F -1 ˙ N P ˙ R D F -1
32 13 21 30 31 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 D ˙ N P ˙ R D F -1 ˙ N P ˙ R D F -1
33 11 32 eqbrtrd 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 ˙ N P ˙ R D F -1
34 10 fveq1i O P = S D P
35 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
36 34 35 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
37 6 7 ltrncnv K HL W H F T F -1 T
38 15 25 37 syl2anc 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 -1 T
39 6 7 ltrnco K HL W H D T F -1 T D F -1 T
40 15 16 38 39 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 D F -1 T
41 2 6 7 8 trlle K HL W H D F -1 T R D F -1 ˙ W
42 15 40 41 syl2anc 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 F -1 ˙ W
43 1 2 3 4 5 6 7 8 9 10 cdlemkoatnle 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 ¬ O P ˙ W
44 43 simprd 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 ˙ W
45 nbrne2 R D F -1 ˙ W ¬ O P ˙ W R D F -1 O P
46 42 44 45 syl2anc 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 F -1 O P
47 46 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 O P R D F -1
48 2 3 5 hlatexch2 K HL O P A N P A R D F -1 A O P R D F -1 O P ˙ N P ˙ R D F -1 N P ˙ O P ˙ R D F -1
49 12 36 24 28 47 48 syl131anc 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 ˙ N P ˙ R D F -1 N P ˙ O P ˙ R D F -1
50 33 49 mpd 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 D F -1
51 6 7 8 trlcocnv K HL W H D T F T R D F -1 = R F D -1
52 15 16 25 51 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 D F -1 = R F D -1
53 52 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 O P ˙ R D F -1 = O P ˙ R F D -1
54 50 53 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 ˙ O P ˙ R F D -1