Metamath Proof Explorer


Theorem cdlemg4f

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 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

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 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
10 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
11 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
12 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
13 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
14 simp33 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 P = P
15 1 2 3 4 5 cdlemg4a K HL W H P A ¬ P ˙ W F T G T F G P = P R F = R G
16 10 11 12 13 14 15 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P R F = R G
17 7 16 eqtr4id K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P V = R F
18 17 oveq2d 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 ˙ V = G Q ˙ R F
19 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
20 1 2 3 4 5 6 7 cdlemg4b12 K HL W H Q A ¬ Q ˙ W G T G Q ˙ V = Q ˙ V
21 10 19 13 20 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 ˙ V = Q ˙ V
22 18 21 eqtr3d 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 ˙ R F = Q ˙ V
23 eqid P ˙ Q ˙ W = P ˙ Q ˙ W
24 3 4 1 6 2 8 23 cdlemg2m K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T G P ˙ G Q ˙ W = P ˙ Q ˙ W
25 10 11 19 13 24 syl121anc 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 ˙ G Q ˙ W = P ˙ Q ˙ W
26 14 25 oveq12d 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 P ˙ G P ˙ G Q ˙ W = P ˙ P ˙ Q ˙ W
27 22 26 oveq12d 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 ˙ R F ˙ F G P ˙ G P ˙ G Q ˙ W = Q ˙ V ˙ P ˙ P ˙ Q ˙ W
28 9 27 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 ˙ P ˙ Q ˙ W