Metamath Proof Explorer


Theorem cdlemk13

Description: Part of proof of Lemma K of Crawley p. 118. Line 13 on p. 119. O , D are k_1, f_1. (Contributed by NM, 1-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
Assertion cdlemk13 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 O P = P ˙ R D ˙ N P ˙ R D F -1

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 10 fveq1i O P = S D P
12 1 2 3 5 6 7 8 4 9 cdlemksv2 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 S D P = P ˙ R D ˙ N P ˙ R D F -1
13 11 12 syl5eq 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 O P = P ˙ R D ˙ N P ˙ R D F -1