Metamath Proof Explorer


Theorem cdlemk13-2N

Description: Part of proof of Lemma K of Crawley p. 118. Line 13 on p. 119. Q , C are k_2, f_2. (Contributed by NM, 1-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
Assertion cdlemk13-2N K HL W H R F = R N F T C T N T R C R F F I B C I B P A ¬ P ˙ W Q P = P ˙ R C ˙ N P ˙ R C F -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 simp11 K HL W H R F = R N F T C T N T R C R F F I B C I B P A ¬ P ˙ W K HL
12 simp12 K HL W H R F = R N F T C T N T R C R F F I B C I B P A ¬ P ˙ W W H
13 11 12 jca K HL W H R F = R N F T C T N T R C R F F I B C I B P A ¬ P ˙ W K HL W H
14 simp21 K HL W H R F = R N F T C T N T R C R F F I B C I B P A ¬ P ˙ W F T
15 simp22 K HL W H R F = R N F T C T N T R C R F F I B C I B P A ¬ P ˙ W C T
16 simp23 K HL W H R F = R N F T C T N T R C R F F I B C I B P A ¬ P ˙ W N T
17 simp33 K HL W H R F = R N F T C T N T R C R F F I B C I B P A ¬ P ˙ W P A ¬ P ˙ W
18 simp13 K HL W H R F = R N F T C T N T R C R F F I B C I B P A ¬ P ˙ W R F = R N
19 simp32l K HL W H R F = R N F T C T N T R C R F F I B C I B P A ¬ P ˙ W F I B
20 simp32r K HL W H R F = R N F T C T N T R C R F F I B C I B P A ¬ P ˙ W C I B
21 simp31 K HL W H R F = R N F T C T N T R C R F F I B C I B P A ¬ P ˙ W R C R F
22 1 2 3 4 5 6 7 8 9 10 cdlemk13 K HL W H F T C T N T P A ¬ P ˙ W R F = R N F I B C I B R C R F Q P = P ˙ R C ˙ N P ˙ R C F -1
23 13 14 15 16 17 18 19 20 21 22 syl333anc K HL W H R F = R N F T C T N T R C R F F I B C I B P A ¬ P ˙ W Q P = P ˙ R C ˙ N P ˙ R C F -1