Metamath Proof Explorer


Theorem cdlemg41

Description: Convert cdlemg40 to function composition. 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 cdlemg41 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 1 2 3 4 5 6 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
8 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T K HL W H
9 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T F T G T
10 simp2ll K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P A
11 1 4 5 6 ltrncoval K HL W H F T G T P A F G P = F G P
12 8 9 10 11 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T F G P = F G P
13 12 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P ˙ F G P = P ˙ F G P
14 13 oveq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T P ˙ F G P ˙ W = P ˙ F G P ˙ W
15 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T Q A
16 1 4 5 6 ltrncoval K HL W H F T G T Q A F G Q = F G Q
17 8 9 15 16 syl3anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T F G Q = F G Q
18 17 oveq2d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T Q ˙ F G Q = Q ˙ F G Q
19 18 oveq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W F T G T Q ˙ F G Q ˙ W = Q ˙ F G Q ˙ W
20 7 14 19 3eqtr4d 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