Metamath Proof Explorer


Theorem cdlemg40

Description: Eliminate P =/= Q conditions from cdlemg39 . TODO: Fix comment. (Contributed by NM, 31-May-2013)

Ref Expression
Hypotheses cdlemg35.l ˙ = K
cdlemg35.j ˙ = join K
cdlemg35.m ˙ = meet K
cdlemg35.a A = Atoms K
cdlemg35.h H = LHyp K
cdlemg35.t T = LTrn K W
Assertion cdlemg40 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P ˙ F G P ˙ W = Q ˙ F G Q ˙ W

Proof

Step Hyp Ref Expression
1 cdlemg35.l ˙ = K
2 cdlemg35.j ˙ = join K
3 cdlemg35.m ˙ = meet K
4 cdlemg35.a A = Atoms K
5 cdlemg35.h H = LHyp K
6 cdlemg35.t T = LTrn K W
7 id P = Q P = Q
8 2fveq3 P = Q F G P = F G Q
9 7 8 oveq12d P = Q P ˙ F G P = Q ˙ F G Q
10 9 oveq1d P = Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
11 10 adantl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P = Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
12 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q K HL W H
13 simpl2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P A ¬ P ˙ W Q A ¬ Q ˙ W
14 simpl3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q F T
15 simpl3r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q G T
16 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P Q
17 eqid trL K W = trL K W
18 1 2 3 4 5 6 17 cdlemg39 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
19 12 13 14 15 16 18 syl113anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P Q P ˙ F G P ˙ W = Q ˙ F G Q ˙ W
20 11 19 pm2.61dane K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P ˙ F G P ˙ W = Q ˙ F G Q ˙ W