Metamath Proof Explorer


Theorem cdlemg4e

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 cdlemg4e 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 = G Q ˙ R F ˙ F G P ˙ G P ˙ G Q ˙ W

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 simp1 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 W H
10 simp23 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P F T
11 simp31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P G T
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 1 2 3 4 ltrnel K HL W H G T P A ¬ P ˙ W G P A ¬ G P ˙ W
14 9 11 12 13 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P G P A ¬ G P ˙ W
15 simp22 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 ¬ Q ˙ W
16 1 2 3 4 ltrnel K HL W H G T Q A ¬ Q ˙ W G Q A ¬ G Q ˙ W
17 9 11 15 16 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P G Q A ¬ G Q ˙ W
18 1 2 3 4 5 6 7 cdlemg4d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P ¬ G Q ˙ G P ˙ F G P
19 1 6 8 2 3 4 5 cdlemc K HL W H F T G P A ¬ G P ˙ W G Q A ¬ G Q ˙ W ¬ G Q ˙ G P ˙ F G P F G Q = G Q ˙ R F ˙ F G P ˙ G P ˙ G Q ˙ W
20 9 10 14 17 18 19 syl131anc 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 = G Q ˙ R F ˙ F G P ˙ G P ˙ G Q ˙ W