Metamath Proof Explorer


Theorem cdlemg14g

Description: TODO: FIX COMMENT. (Contributed by NM, 22-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 cdlemg14g K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P 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 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P K HL W H
9 simp31 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P F T
10 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P P A ¬ P ˙ W
11 simp2r K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P Q A ¬ Q ˙ W
12 1 2 3 4 5 6 ltrnu K HL W H F T P A ¬ P ˙ W Q A ¬ Q ˙ W P ˙ F P ˙ W = Q ˙ F Q ˙ W
13 8 9 10 11 12 syl211anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P P ˙ F P ˙ W = Q ˙ F Q ˙ W
14 simp33 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P G P = P
15 14 fveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P F G P = F P
16 15 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P P ˙ F G P = P ˙ F P
17 16 oveq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P P ˙ F G P ˙ W = P ˙ F P ˙ W
18 simp32 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P G T
19 1 4 5 6 ltrnateq K HL W H G T P A ¬ P ˙ W Q A ¬ Q ˙ W G P = P G Q = Q
20 8 18 10 11 14 19 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P G Q = Q
21 20 fveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P F G Q = F Q
22 21 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P Q ˙ F G Q = Q ˙ F Q
23 22 oveq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P Q ˙ F G Q ˙ W = Q ˙ F Q ˙ W
24 13 17 23 3eqtr4d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T G P = P P ˙ F G P ˙ W = Q ˙ F G Q ˙ W