Metamath Proof Explorer


Theorem cdlemg6a

Description: TODO: FIX COMMENT. TODO: replace with cdlemg4 . (Contributed by NM, 27-Apr-2013)

Ref Expression
Hypotheses cdlemg4.l ˙ = K
cdlemg4.a A = Atoms K
cdlemg4.h H = LHyp K
cdlemg4.t T = LTrn K W
cdlemg4.r R = trL K W
cdlemg4.j ˙ = join K
cdlemg4b.v V = R G
Assertion cdlemg6a K HL W H P A ¬ P ˙ W r A ¬ r ˙ W F T G T ¬ r ˙ P ˙ V F G P = P F G r = r

Proof

Step Hyp Ref Expression
1 cdlemg4.l ˙ = K
2 cdlemg4.a A = Atoms K
3 cdlemg4.h H = LHyp K
4 cdlemg4.t T = LTrn K W
5 cdlemg4.r R = trL K W
6 cdlemg4.j ˙ = join K
7 cdlemg4b.v V = R G
8 1 2 3 4 5 6 7 cdlemg4 K HL W H P A ¬ P ˙ W r A ¬ r ˙ W F T G T ¬ r ˙ P ˙ V F G P = P F G r = r