Metamath Proof Explorer


Theorem cdlemg10b

Description: TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in ltrn* area? (Contributed by NM, 4-May-2013)

Ref Expression
Hypotheses cdlemg8.l ˙ = K
cdlemg8.j ˙ = join K
cdlemg8.m ˙ = meet K
cdlemg8.a A = Atoms K
cdlemg8.h H = LHyp K
cdlemg8.t T = LTrn K W
Assertion cdlemg10b K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T F P ˙ F Q ˙ W = P ˙ Q ˙ W

Proof

Step Hyp Ref Expression
1 cdlemg8.l ˙ = K
2 cdlemg8.j ˙ = join K
3 cdlemg8.m ˙ = meet K
4 cdlemg8.a A = Atoms K
5 cdlemg8.h H = LHyp K
6 cdlemg8.t T = LTrn K W
7 eqid P ˙ Q ˙ W = P ˙ Q ˙ W
8 5 6 1 2 4 3 7 cdlemg2m K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T F P ˙ F Q ˙ W = P ˙ Q ˙ W