Metamath Proof Explorer


Theorem cdlemg16z

Description: Eliminate ( ( F( GP ) ) .\/ ( F( GQ ) ) ) =/= ( P .\/ Q ) condition from cdlemg16 . TODO: would it help to also eliminate P =/= Q here or later? (Contributed by NM, 25-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 cdlemg16z K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W

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 simpl11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F G P ˙ F G Q = P ˙ Q K HL W H
9 simpl12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F G P ˙ F G Q = P ˙ Q P A ¬ P ˙ W
10 simpl13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F G P ˙ F G Q = P ˙ Q Q A ¬ Q ˙ W
11 simpl21 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F G P ˙ F G Q = P ˙ Q F T
12 simpl22 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F G P ˙ F G Q = P ˙ Q G T
13 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F G P ˙ F G Q = P ˙ Q F G P ˙ F G Q = P ˙ Q
14 1 2 3 4 5 6 cdlemg8 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T F G P ˙ F G Q = P ˙ Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
15 8 9 10 11 12 13 14 syl132anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F G P ˙ F G Q = P ˙ Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
16 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F G P ˙ F G Q P ˙ Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
17 simpl2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F G P ˙ F G Q P ˙ Q F T G T P Q
18 simpl3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F G P ˙ F G Q P ˙ Q ¬ R F ˙ P ˙ Q
19 simpl3r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F G P ˙ F G Q P ˙ Q ¬ R G ˙ P ˙ Q
20 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F G P ˙ F G Q P ˙ Q F G P ˙ F G Q P ˙ Q
21 1 2 3 4 5 6 7 cdlemg16 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F G P ˙ F G Q P ˙ Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
22 16 17 18 19 20 21 syl113anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q F G P ˙ F G Q P ˙ Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
23 15 22 pm2.61dane K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q ¬ R F ˙ P ˙ Q ¬ R G ˙ P ˙ Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W