Metamath Proof Explorer


Theorem cdlemg4d

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

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 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
9 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
10 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
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 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P ¬ Q ˙ P ˙ V
13 1 2 3 4 5 6 7 cdlemg4c K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T ¬ Q ˙ P ˙ V ¬ G Q ˙ P ˙ V
14 8 9 10 11 12 13 syl131anc 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 ˙ P ˙ V
15 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
16 simp21l 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
17 1 2 3 4 ltrnel K HL W H G T P A ¬ P ˙ W G P A ¬ G P ˙ W
18 17 simpld K HL W H G T P A ¬ P ˙ W G P A
19 8 11 9 18 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
20 6 2 hlatjcom K HL P A G P A P ˙ G P = G P ˙ P
21 15 16 19 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 P ˙ G P = G P ˙ P
22 1 2 3 4 5 6 7 cdlemg4b1 K HL W H P A ¬ P ˙ W G T P ˙ V = P ˙ G P
23 8 9 11 22 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T ¬ Q ˙ P ˙ V F G P = P P ˙ V = P ˙ G P
24 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
25 24 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 P ˙ F G P = G P ˙ P
26 21 23 25 3eqtr4rd 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 ˙ F G P = P ˙ V
27 26 breq2d 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 G Q ˙ P ˙ V
28 14 27 mtbird 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