Metamath Proof Explorer


Theorem cdlemk32

Description: Part of proof of Lemma K of Crawley p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. (Contributed by NM, 17-Jul-2013)

Ref Expression
Hypotheses cdlemk3.b B = Base K
cdlemk3.l ˙ = K
cdlemk3.j ˙ = join K
cdlemk3.m ˙ = meet K
cdlemk3.a A = Atoms K
cdlemk3.h H = LHyp K
cdlemk3.t T = LTrn K W
cdlemk3.r R = trL K W
cdlemk3.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
cdlemk3.u1 Y = d T , e T ι j T | j P = P ˙ R e ˙ S d P ˙ R e d -1
Assertion cdlemk32 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 Y G P = P ˙ R G ˙ P ˙ R b ˙ N P ˙ R b F -1 ˙ R G b -1

Proof

Step Hyp Ref Expression
1 cdlemk3.b B = Base K
2 cdlemk3.l ˙ = K
3 cdlemk3.j ˙ = join K
4 cdlemk3.m ˙ = meet K
5 cdlemk3.a A = Atoms K
6 cdlemk3.h H = LHyp K
7 cdlemk3.t T = LTrn K W
8 cdlemk3.r R = trL K W
9 cdlemk3.s S = f T ι i T | i P = P ˙ R f ˙ N P ˙ R f F -1
10 cdlemk3.u1 Y = d T , e T ι j T | j P = P ˙ R e ˙ S d P ˙ R e d -1
11 1 2 3 4 5 6 7 8 9 10 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 Y G P = P ˙ R G ˙ S b P ˙ R G b -1
12 simp1 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 K HL W H R F = R N
13 simp2l 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 F T b T N T
14 simp31l 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 R b R F
15 simp321 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 F I B
16 simp322 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 I B
17 15 16 jca 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 F I B b I B
18 simp33 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 P A ¬ P ˙ W
19 1 2 3 4 5 6 7 8 9 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
20 12 13 14 17 18 19 syl113anc 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 S b P = P ˙ R b ˙ N P ˙ R b F -1
21 20 oveq1d 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 S b P ˙ R G b -1 = P ˙ R b ˙ N P ˙ R b F -1 ˙ R G b -1
22 21 oveq2d 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 P ˙ R G ˙ S b P ˙ R G b -1 = P ˙ R G ˙ P ˙ R b ˙ N P ˙ R b F -1 ˙ R G b -1
23 11 22 eqtrd 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 Y G P = P ˙ R G ˙ P ˙ R b ˙ N P ˙ R b F -1 ˙ R G b -1