Theorem tendopl2

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

	Ref	Expression
Hypotheses	tendoplcbv.p	⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
	tendopl2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion	tendopl2	⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tendoplcbv.p	⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
2		tendopl2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3	1 2	tendopl	⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) → ( 𝑈 𝑃 𝑉 ) = ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) ) )
4	3	3adant3	⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( 𝑈 𝑃 𝑉 ) = ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) ) )
5		fveq2	⊢ ( 𝑔 = 𝐹 → ( 𝑈 ‘ 𝑔 ) = ( 𝑈 ‘ 𝐹 ) )
6		fveq2	⊢ ( 𝑔 = 𝐹 → ( 𝑉 ‘ 𝑔 ) = ( 𝑉 ‘ 𝐹 ) )
7	5 6	coeq12d	⊢ ( 𝑔 = 𝐹 → ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )
8	7	adantl	⊢ ( ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑔 = 𝐹 ) → ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )
9		simp3	⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ 𝑇 )
10		fvex	⊢ ( 𝑈 ‘ 𝐹 ) ∈ V
11		fvex	⊢ ( 𝑉 ‘ 𝐹 ) ∈ V
12	10 11	coex	⊢ ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) ∈ V
13	12	a1i	⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) ∈ V )
14	4 8 9 13	fvmptd	⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ) → ( ( 𝑈 𝑃 𝑉 ) ‘ 𝐹 ) = ( ( 𝑈 ‘ 𝐹 ) ∘ ( 𝑉 ‘ 𝐹 ) ) )