Metamath Proof Explorer


Theorem cdlemk18

Description: Part of proof of Lemma K of Crawley p. 118. Line 22 on p. 119. N , U , O , D are k, sigma_1 (p), k_1, f_1. (Contributed by NM, 2-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
Assertion cdlemk18 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F N P = U F 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 1 2 3 4 5 6 7 8 9 10 cdlemk17 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F N P = P ˙ R F ˙ O P ˙ R F D -1
13 simp11 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F K HL W H
14 simp23 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F R F = R N
15 simp12 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F F T
16 simp13 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F D T
17 simp21 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F N T
18 simp33 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F R D R F
19 18 18 jca K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F R D R F R D R F
20 simp31 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F F I B
21 simp32 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F D I B
22 20 20 21 3jca K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F F I B F I B D I B
23 simp22 K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F P A ¬ P ˙ W
24 1 2 3 4 5 6 7 8 9 10 11 cdlemkuv2 K HL W H R F = R N F T F T D T N T R D R F R D R F F I B F I B D I B P A ¬ P ˙ W U F P = P ˙ R F ˙ O P ˙ R F D -1
25 13 14 15 15 16 17 19 22 23 24 syl333anc K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F U F P = P ˙ R F ˙ O P ˙ R F D -1
26 12 25 eqtr4d K HL W H F T D T N T P A ¬ P ˙ W R F = R N F I B D I B R D R F N P = U F P