Metamath Proof Explorer


Theorem cdlemg4g

Description: TODO: FIX COMMENT. (Contributed by NM, 25-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
cdlemg4.m ˙ = meet K
Assertion cdlemg4g K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P F G Q = Q ˙ V ˙ P ˙ Q

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 cdlemg4.m ˙ = meet K
9 1 2 3 4 5 6 7 8 cdlemg4f K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P F G Q = Q ˙ V ˙ P ˙ P ˙ Q ˙ W
10 simp1l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P K HL
11 simp1r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P W H
12 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P P A ¬ P ˙ W
13 simp22l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P Q A
14 eqid P ˙ Q ˙ W = P ˙ Q ˙ W
15 1 6 8 2 3 14 cdleme0cp K HL W H P A ¬ P ˙ W Q A P ˙ P ˙ Q ˙ W = P ˙ Q
16 10 11 12 13 15 syl22anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P P ˙ P ˙ Q ˙ W = P ˙ Q
17 16 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P Q ˙ V ˙ P ˙ P ˙ Q ˙ W = Q ˙ V ˙ P ˙ Q
18 9 17 eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P F G Q = Q ˙ V ˙ P ˙ Q