Metamath Proof Explorer


Theorem cdlemg17e

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

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 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
9 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
10 simp13 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 Q A ¬ Q ˙ W
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 eqid P ˙ Q ˙ W = P ˙ Q ˙ W
13 5 6 1 2 4 3 12 cdlemg2k K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T F P ˙ F Q = F P ˙ P ˙ Q ˙ W
14 8 9 10 11 13 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 F P ˙ F Q = F P ˙ P ˙ Q ˙ W
15 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
16 1 2 3 4 5 6 7 trlval2 K HL W H G T P A ¬ P ˙ W R G = P ˙ G P ˙ W
17 8 15 9 16 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 = P ˙ G P ˙ W
18 simp1 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 P A ¬ P ˙ W Q A ¬ Q ˙ W
19 simp23 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 Q
20 simp31 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 P P
21 simp32 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 ˙ P ˙ Q
22 simp33 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 A ¬ r ˙ W P ˙ r = Q ˙ r
23 1 2 3 4 5 6 7 cdlemg17b K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G T P Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r G P = Q
24 18 15 19 20 21 22 23 syl123anc 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 P = Q
25 24 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 P ˙ G P = P ˙ Q
26 25 oveq1d 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 ˙ G P ˙ W = P ˙ Q ˙ W
27 17 26 eqtrd 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 = P ˙ Q ˙ W
28 27 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 ˙ P ˙ Q ˙ W
29 14 28 eqtr4d 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