Metamath Proof Explorer

Theorem tendopl

Description: Value of endomorphism sum operation. (Contributed by NM, 10-Jun-2013)

Ref Expression
Hypotheses tendoplcbv.p ⊢ P = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
tendopl2.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion tendopl ⊢ U ∈ E ∧ V ∈ E → U P V = g ∈ T ⟼ U ⁡ g ∘ V ⁡ g

Proof

Step Hyp Ref Expression
1 tendoplcbv.p ⊢ P = s ∈ E , t ∈ E ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
2 tendopl2.t ⊢ T = LTrn ⁡ K ⁡ W
3 fveq1 ⊢ u = U → u ⁡ g = U ⁡ g
4 3 coeq1d ⊢ u = U → u ⁡ g ∘ v ⁡ g = U ⁡ g ∘ v ⁡ g
5 4 mpteq2dv ⊢ u = U → g ∈ T ⟼ u ⁡ g ∘ v ⁡ g = g ∈ T ⟼ U ⁡ g ∘ v ⁡ g
6 fveq1 ⊢ v = V → v ⁡ g = V ⁡ g
7 6 coeq2d ⊢ v = V → U ⁡ g ∘ v ⁡ g = U ⁡ g ∘ V ⁡ g
8 7 mpteq2dv ⊢ v = V → g ∈ T ⟼ U ⁡ g ∘ v ⁡ g = g ∈ T ⟼ U ⁡ g ∘ V ⁡ g
9 1 tendoplcbv ⊢ P = u ∈ E , v ∈ E ⟼ g ∈ T ⟼ u ⁡ g ∘ v ⁡ g
10 2 fvexi ⊢ T ∈ V
11 10 mptex ⊢ g ∈ T ⟼ U ⁡ g ∘ V ⁡ g ∈ V
12 5 8 9 11 ovmpo ⊢ U ∈ E ∧ V ∈ E → U P V = g ∈ T ⟼ U ⁡ g ∘ V ⁡ g