Metamath Proof Explorer


Theorem cdlemk12u-2N

Description: Part of proof of Lemma K of Crawley p. 118. Line 18, p. 119, showing Eq. 4 (line 10, p. 119) for the sigma_2 ( V ) case. (Contributed by NM, 5-Jul-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemk2.b B = Base K
cdlemk2.l ˙ = K
cdlemk2.j ˙ = join K
cdlemk2.m ˙ = meet K
cdlemk2.a A = Atoms K
cdlemk2.h H = LHyp K
cdlemk2.t T = LTrn K W
cdlemk2.r R = trL K W
cdlemk2.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
cdlemk2.q Q = S C
cdlemk2.v V = d T ι k T | k P = P ˙ R d ˙ Q P ˙ R d C -1
Assertion cdlemk12u-2N K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W V G P = P ˙ G P ˙ V X P ˙ R X G -1

Proof

Step Hyp Ref Expression
1 cdlemk2.b B = Base K
2 cdlemk2.l ˙ = K
3 cdlemk2.j ˙ = join K
4 cdlemk2.m ˙ = meet K
5 cdlemk2.a A = Atoms K
6 cdlemk2.h H = LHyp K
7 cdlemk2.t T = LTrn K W
8 cdlemk2.r R = trL K W
9 cdlemk2.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
10 cdlemk2.q Q = S C
11 cdlemk2.v V = d T ι k T | k P = P ˙ R d ˙ Q P ˙ R d C -1
12 simp11 K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W K HL
13 simp12 K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W W H
14 12 13 jca K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W K HL W H
15 simp211 K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W F T
16 simp212 K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W C T
17 simp213 K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W N T
18 simp22l K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W G T
19 simp23l K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W X T
20 17 18 19 3jca K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W N T G T X T
21 simp33 K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W P A ¬ P ˙ W
22 simp13 K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W R F = R N
23 simp322 K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W F I B
24 simp323 K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W C I B
25 simp22r K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W G I B
26 23 24 25 3jca K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W F I B C I B G I B
27 simp23r K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W X I B
28 simp321 K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W R G R X
29 27 28 jca K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W X I B R G R X
30 simp31 K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W R C R F R G R C R X R C
31 1 2 3 4 5 6 7 8 9 10 11 cdlemk12u K HL W H F T C T N T G T X T P A ¬ P ˙ W R F = R N F I B C I B G I B X I B R G R X R C R F R G R C R X R C V G P = P ˙ G P ˙ V X P ˙ R X G -1
32 14 15 16 20 21 22 26 29 30 31 syl333anc K HL W H R F = R N F T C T N T G T G I B X T X I B R C R F R G R C R X R C R G R X F I B C I B P A ¬ P ˙ W V G P = P ˙ G P ˙ V X P ˙ R X G -1