Metamath Proof Explorer


Theorem cdlemg17i

Description: TODO: fix comment. (Contributed by NM, 10-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 cdlemg17i 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 = F Q

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 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
10 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
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 1 4 5 6 ltrnel K HL W H F T P A ¬ P ˙ W F P A ¬ F P ˙ W
13 8 11 10 12 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
14 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
15 1 4 5 6 ltrnatneq K HL W H G T P A ¬ P ˙ W F P A ¬ F P ˙ W G P P G F P F P
16 8 9 10 13 14 15 syl131anc 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 F P
17 16 neneqd 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 = F P
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 1 4 5 6 ltrnel K HL W H G T F P A ¬ F P ˙ W G F P A ¬ G F P ˙ W
20 8 9 13 19 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 G F P A ¬ G F P ˙ W
21 11 9 jca 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 G T
22 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
23 1 2 3 4 5 6 7 cdlemg17g 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 ˙ F P ˙ F Q
24 22 23 jca 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 G F P ˙ F P ˙ F Q
25 simp3 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 R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r
26 1 2 3 4 5 6 7 cdlemg17h K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W G F P A ¬ G F P ˙ W F T G T P Q G F P ˙ F P ˙ F Q G P P R G ˙ P ˙ Q ¬ r A ¬ r ˙ W P ˙ r = Q ˙ r G F P = F P G F P = F Q
27 18 20 21 24 25 26 syl131anc 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 = F P G F P = F Q
28 27 ord 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 = F P G F P = F Q
29 17 28 mpd 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 = F Q