Metamath Proof Explorer


Theorem cdlemk21N

Description: Part of proof of Lemma K of Crawley p. 118. Lines 26-27, p. 119 for i=0 and j=1. (Contributed by NM, 5-Jul-2013) (New usage is discouraged.)

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