Metamath Proof Explorer

Theorem tendopl2

Description: Value of result 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 tendopl2 ⊢ U ∈ E ∧ V ∈ E ∧ F ∈ T → U P V ⁡ F = U ⁡ F ∘ V ⁡ F

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 1 2 tendopl ⊢ U ∈ E ∧ V ∈ E → U P V = g ∈ T ⟼ U ⁡ g ∘ V ⁡ g
4 3 3adant3 ⊢ U ∈ E ∧ V ∈ E ∧ F ∈ T → U P V = g ∈ T ⟼ U ⁡ g ∘ V ⁡ g
5 fveq2 ⊢ g = F → U ⁡ g = U ⁡ F
6 fveq2 ⊢ g = F → V ⁡ g = V ⁡ F
7 5 6 coeq12d ⊢ g = F → U ⁡ g ∘ V ⁡ g = U ⁡ F ∘ V ⁡ F
8 7 adantl ⊢ U ∈ E ∧ V ∈ E ∧ F ∈ T ∧ g = F → U ⁡ g ∘ V ⁡ g = U ⁡ F ∘ V ⁡ F
9 simp3 ⊢ U ∈ E ∧ V ∈ E ∧ F ∈ T → F ∈ T
10 fvex ⊢ U ⁡ F ∈ V
11 fvex ⊢ V ⁡ F ∈ V
12 10 11 coex ⊢ U ⁡ F ∘ V ⁡ F ∈ V
13 12 a1i ⊢ U ∈ E ∧ V ∈ E ∧ F ∈ T → U ⁡ F ∘ V ⁡ F ∈ V
14 4 8 9 13 fvmptd ⊢ U ∈ E ∧ V ∈ E ∧ F ∈ T → U P V ⁡ F = U ⁡ F ∘ V ⁡ F