Metamath Proof Explorer


Theorem cdlemg17f

Description: TODO: fix comment. (Contributed by NM, 8-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 cdlemg17f K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r F P ˙ F Q = F P ˙ G F P

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 cdlemg17e K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r F P ˙ F Q = F P ˙ R G
9 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r K HL W H
10 simp22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r G T
11 simp21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r F T
12 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A ¬ P ˙ W
13 1 4 5 6 ltrnel K HL W H F T P A ¬ P ˙ W F P A ¬ F P ˙ W
14 9 11 12 13 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r F P A ¬ F P ˙ W
15 1 2 3 4 5 6 7 trlval2 K HL W H G T F P A ¬ F P ˙ W R G = F P ˙ G F P ˙ W
16 9 10 14 15 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r R G = F P ˙ G F P ˙ W
17 16 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r F P ˙ R G = F P ˙ F P ˙ G F P ˙ W
18 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r P A
19 1 4 5 6 ltrncoat K HL W H G T F T P A G F P A
20 9 10 11 18 19 syl121anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r G F P A
21 eqid F P ˙ G F P ˙ W = F P ˙ G F P ˙ W
22 1 2 3 4 5 21 cdleme0cp K HL W H F P A ¬ F P ˙ W G F P A F P ˙ F P ˙ G F P ˙ W = F P ˙ G F P
23 9 14 20 22 syl12anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r F P ˙ F P ˙ G F P ˙ W = F P ˙ G F P
24 8 17 23 3eqtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r F P ˙ F Q = F P ˙ G F P