Theorem tendopl

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

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

Proof

Step	Hyp	Ref	Expression
1		tendoplcbv.p	⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
2		tendopl2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3		fveq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 ‘ 𝑔 ) = ( 𝑈 ‘ 𝑔 ) )
4	3	coeq1d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) = ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) )
5	4	mpteq2dv	⊢ ( 𝑢 = 𝑈 → ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑢 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) ) = ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) ) )
6		fveq1	⊢ ( 𝑣 = 𝑉 → ( 𝑣 ‘ 𝑔 ) = ( 𝑉 ‘ 𝑔 ) )
7	6	coeq2d	⊢ ( 𝑣 = 𝑉 → ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) = ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) )
8	7	mpteq2dv	⊢ ( 𝑣 = 𝑉 → ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) ) = ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) ) )
9	1	tendoplcbv	⊢ 𝑃 = ( 𝑢 ∈ 𝐸 , 𝑣 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑢 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) ) )
10	2	fvexi	⊢ 𝑇 ∈ V
11	10	mptex	⊢ ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) ) ∈ V
12	5 8 9 11	ovmpo	⊢ ( ( 𝑈 ∈ 𝐸 ∧ 𝑉 ∈ 𝐸 ) → ( 𝑈 𝑃 𝑉 ) = ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑈 ‘ 𝑔 ) ∘ ( 𝑉 ‘ 𝑔 ) ) ) )