Metamath Proof Explorer


Theorem cdlemk20

Description: Part of proof of Lemma K of Crawley p. 118. Line 22, p. 119 for the i=2, j=1 case. Note typo on line 22: f should be f_i. Our D , C , O , Q , U , V represent their f_1, f_2, k_1, k_2, sigma_1, sigma_2. (Contributed by NM, 5-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
cdlemk2a.q Q = S C
Assertion cdlemk20 K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D U C P = Q P

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 cdlemk2a.q Q = S C
13 simp11 K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D K HL W H
14 simp23 K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D R F = R N
15 simp21r K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D C T
16 simp12 K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D F T
17 simp13 K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D D T
18 simp21l K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D N T
19 simp3r1 K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D R D R F
20 simp3r3 K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D R C R D
21 20 necomd K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D R D R C
22 19 21 jca K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D R D R F R D R C
23 simp3l1 K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D F I B
24 simp3l3 K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D C I B
25 simp3l2 K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D D I B
26 23 24 25 3jca K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D F I B C I B D I B
27 simp22 K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D P A ¬ P ˙ W
28 1 2 3 4 5 6 7 8 9 10 11 cdlemkuv2 K HL W H R F = R N C T F T D T N T R D R F R D R C F I B C I B D I B P A ¬ P ˙ W U C P = P ˙ R C ˙ O P ˙ R C D -1
29 13 14 15 16 17 18 22 26 27 28 syl333anc K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D U C P = P ˙ R C ˙ O P ˙ R C D -1
30 2 3 5 6 7 8 trljat1 K HL W H C T P A ¬ P ˙ W P ˙ R C = P ˙ C P
31 13 15 27 30 syl3anc K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D P ˙ R C = P ˙ C P
32 10 fveq1i O P = S D P
33 32 a1i K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D O P = S D P
34 6 7 8 trlcocnv K HL W H C T D T R C D -1 = R D C -1
35 13 15 17 34 syl3anc K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D R C D -1 = R D C -1
36 33 35 oveq12d K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D O P ˙ R C D -1 = S D P ˙ R D C -1
37 31 36 oveq12d K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D P ˙ R C ˙ O P ˙ R C D -1 = P ˙ C P ˙ S D P ˙ R D C -1
38 12 fveq1i Q P = S C P
39 18 17 jca K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D N T D T
40 simp3r2 K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D R C R F
41 40 19 jca K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D R C R F R D R F
42 1 2 3 5 6 7 8 4 9 cdlemk12 K HL W H F T C T N T D T P A ¬ P ˙ W R F = R N F I B C I B D I B R C R F R D R F R C R D S C P = P ˙ C P ˙ S D P ˙ R D C -1
43 13 16 15 39 27 14 26 41 20 42 syl333anc K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D S C P = P ˙ C P ˙ S D P ˙ R D C -1
44 38 43 eqtr2id K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D P ˙ C P ˙ S D P ˙ R D C -1 = Q P
45 29 37 44 3eqtrd K HL W H F T D T N T C T P A ¬ P ˙ W R F = R N F I B D I B C I B R D R F R C R F R C R D U C P = Q P