Metamath Proof Explorer


Theorem cdlemkyyN

Description: Part of proof of Lemma K of Crawley p. 118. TODO: clean up ( b Y G ) stuff. (Contributed by NM, 21-Jul-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemk5.b B = Base K
cdlemk5.l ˙ = K
cdlemk5.j ˙ = join K
cdlemk5.m ˙ = meet K
cdlemk5.a A = Atoms K
cdlemk5.h H = LHyp K
cdlemk5.t T = LTrn K W
cdlemk5.r R = trL K W
cdlemk5.z Z = P ˙ R b ˙ N P ˙ R b F -1
cdlemk5.y Y = P ˙ R g ˙ Z ˙ R g b -1
cdlemk5.x X = ι z T | b T b I B R b R F R b R g z P = Y
cdlemk5a.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
cdlemk5a.u1 V = d T , e T ι j T | j P = P ˙ R e ˙ S d P ˙ R e d -1
Assertion cdlemkyyN K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G G / g X P = b V G P

Proof

Step Hyp Ref Expression
1 cdlemk5.b B = Base K
2 cdlemk5.l ˙ = K
3 cdlemk5.j ˙ = join K
4 cdlemk5.m ˙ = meet K
5 cdlemk5.a A = Atoms K
6 cdlemk5.h H = LHyp K
7 cdlemk5.t T = LTrn K W
8 cdlemk5.r R = trL K W
9 cdlemk5.z Z = P ˙ R b ˙ N P ˙ R b F -1
10 cdlemk5.y Y = P ˙ R g ˙ Z ˙ R g b -1
11 cdlemk5.x X = ι z T | b T b I B R b R F R b R g z P = Y
12 cdlemk5a.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
13 cdlemk5a.u1 V = d T , e T ι j T | j P = P ˙ R e ˙ S d P ˙ R e d -1
14 simp11 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G K HL
15 simp12 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G W H
16 14 15 jca K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G K HL W H
17 simp13 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G R F = R N
18 simp211 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G F T
19 simp3l K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G b T
20 simp213 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G N T
21 simp3r2 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G R b R F
22 simp212 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G F I B
23 simp3r1 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G b I B
24 22 23 jca K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G F I B b I B
25 simp23 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G P A ¬ P ˙ W
26 1 2 3 4 5 6 7 8 12 cdlemk30 K HL W H R F = R N F T b T N T R b R F F I B b I B P A ¬ P ˙ W S b P = P ˙ R b ˙ N P ˙ R b F -1
27 16 17 18 19 20 21 24 25 26 syl233anc K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G S b P = P ˙ R b ˙ N P ˙ R b F -1
28 27 9 eqtr4di K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G S b P = Z
29 28 oveq1d K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G S b P ˙ R G b -1 = Z ˙ R G b -1
30 29 oveq2d K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G P ˙ R G ˙ S b P ˙ R G b -1 = P ˙ R G ˙ Z ˙ R G b -1
31 18 19 20 3jca K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G F T b T N T
32 simp22l K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G G T
33 simp3r3 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G R b R G
34 21 33 jca K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G R b R F R b R G
35 simp22r K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G G I B
36 22 23 35 3jca K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G F I B b I B G I B
37 1 2 3 4 5 6 7 8 12 13 cdlemk31 K HL W H R F = R N F T b T N T G T R b R F R b R G F I B b I B G I B P A ¬ P ˙ W b V G P = P ˙ R G ˙ S b P ˙ R G b -1
38 16 17 31 32 34 36 25 37 syl223anc K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G b V G P = P ˙ R G ˙ S b P ˙ R G b -1
39 18 22 jca K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G F T F I B
40 simp22 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G G T G I B
41 simp3 K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G b T b I B R b R F R b R G
42 1 2 3 4 5 6 7 8 9 10 11 cdlemk42yN K HL W H F T F I B G T G I B N T P A ¬ P ˙ W R F = R N b T b I B R b R F R b R G G / g X P = P ˙ R G ˙ Z ˙ R G b -1
43 16 39 40 20 25 17 41 42 syl331anc K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G G / g X P = P ˙ R G ˙ Z ˙ R G b -1
44 30 38 43 3eqtr4rd K HL W H R F = R N F T F I B N T G T G I B P A ¬ P ˙ W b T b I B R b R F R b R G G / g X P = b V G P