Metamath Proof Explorer


Theorem cdlemkuat

Description: Part of proof of Lemma K of Crawley p. 118. (Contributed by NM, 4-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 cdlemkuat K HL W H R F = R N G T F T D T N T R D R F R D R G F I B G I B D I B P A ¬ P ˙ W U G P A

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 simp11 K HL W H R F = R N G T F T D T N T R D R F R D R G F I B G I B D I B P A ¬ P ˙ W K HL W H
13 1 2 3 4 5 6 7 8 9 10 11 cdlemkuel K HL W H R F = R N G T F T D T N T R D R F R D R G F I B G I B D I B P A ¬ P ˙ W U G T
14 simp33l K HL W H R F = R N G T F T D T N T R D R F R D R G F I B G I B D I B P A ¬ P ˙ W P A
15 2 5 6 7 ltrnat K HL W H U G T P A U G P A
16 12 13 14 15 syl3anc K HL W H R F = R N G T F T D T N T R D R F R D R G F I B G I B D I B P A ¬ P ˙ W U G P A