Metamath Proof Explorer


Theorem cdlemg26zz

Description: cdlemg16zz restated for easier studying. TODO: Discard this after everything is figured out. (Contributed by NM, 26-May-2013)

Ref Expression
Hypotheses cdlemg12.l ˙ = K
cdlemg12.j ˙ = join K
cdlemg12.m ˙ = meet K
cdlemg12.a A = Atoms K
cdlemg12.h H = LHyp K
cdlemg12.t T = LTrn K W
cdlemg12b.r R = trL K W
Assertion cdlemg26zz K HL W H Q A ¬ Q ˙ W z A ¬ z ˙ W F T G T ¬ R F ˙ Q ˙ z ¬ R G ˙ Q ˙ z Q ˙ F G Q ˙ W = z ˙ F G z ˙ W

Proof

Step Hyp Ref Expression
1 cdlemg12.l ˙ = K
2 cdlemg12.j ˙ = join K
3 cdlemg12.m ˙ = meet K
4 cdlemg12.a A = Atoms K
5 cdlemg12.h H = LHyp K
6 cdlemg12.t T = LTrn K W
7 cdlemg12b.r R = trL K W
8 1 2 3 4 5 6 7 cdlemg25zz K HL W H Q A ¬ Q ˙ W z A ¬ z ˙ W F T G T ¬ R F ˙ Q ˙ z ¬ R G ˙ Q ˙ z Q ˙ F G Q ˙ W = z ˙ F G z ˙ W