Metamath Proof Explorer

Theorem tendoplco2

Description: Value of result of endomorphism sum operation on a translation composition. (Contributed by NM, 10-Jun-2013)

Ref Expression
Hypotheses tendopl.h ⊢H=LHyp⁡K
tendopl.t ⊢T=LTrn⁡K⁡W
tendopl.e ⊢E=TEndo⁡K⁡W
tendopl.p ⊢P=s∈E,t∈E⟼f∈T⟼s⁡f∘t⁡f
Assertion tendoplco2 ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T∧G∈T→UPV⁡F∘G=UPV⁡F∘UPV⁡G

Proof

Step Hyp Ref Expression
1 tendopl.h ⊢H=LHyp⁡K
2 tendopl.t ⊢T=LTrn⁡K⁡W
3 tendopl.e ⊢E=TEndo⁡K⁡W
4 tendopl.p ⊢P=s∈E,t∈E⟼f∈T⟼s⁡f∘t⁡f
5 1 2 3 tendoco2 ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T∧G∈T→U⁡F∘G∘V⁡F∘G=U⁡F∘V⁡F∘U⁡G∘V⁡G
6 simp1 ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T∧G∈T→K∈HL∧W∈H
7 simp3l ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T∧G∈T→F∈T
8 simp3r ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T∧G∈T→G∈T
9 1 2 ltrnco ⊢K∈HL∧W∈H∧F∈T∧G∈T→F∘G∈T
10 6 7 8 9 syl3anc ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T∧G∈T→F∘G∈T
11 simp2l ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∘G∈T→U∈E
12 simp2r ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∘G∈T→V∈E
13 simp3 ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∘G∈T→F∘G∈T
14 4 2 tendopl2 ⊢U∈E∧V∈E∧F∘G∈T→UPV⁡F∘G=U⁡F∘G∘V⁡F∘G
15 11 12 13 14 syl3anc ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∘G∈T→UPV⁡F∘G=U⁡F∘G∘V⁡F∘G
16 10 15 syld3an3 ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T∧G∈T→UPV⁡F∘G=U⁡F∘G∘V⁡F∘G
17 simp2l ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T∧G∈T→U∈E
18 simp2r ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T∧G∈T→V∈E
19 4 2 tendopl2 ⊢U∈E∧V∈E∧F∈T→UPV⁡F=U⁡F∘V⁡F
20 17 18 7 19 syl3anc ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T∧G∈T→UPV⁡F=U⁡F∘V⁡F
21 4 2 tendopl2 ⊢U∈E∧V∈E∧G∈T→UPV⁡G=U⁡G∘V⁡G
22 17 18 8 21 syl3anc ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T∧G∈T→UPV⁡G=U⁡G∘V⁡G
23 20 22 coeq12d ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T∧G∈T→UPV⁡F∘UPV⁡G=U⁡F∘V⁡F∘U⁡G∘V⁡G
24 5 16 23 3eqtr4d ⊢K∈HL∧W∈H∧U∈E∧V∈E∧F∈T∧G∈T→UPV⁡F∘G=UPV⁡F∘UPV⁡G