Theorem tendoplcbv

Description: Define sum operation for trace-preserving endomorphisms. Change bound variables to isolate them later. (Contributed by NM, 11-Jun-2013)

	Ref	Expression
Hypothesis	tendoplcbv.p	⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
Assertion	tendoplcbv	⊢ 𝑃 = ( 𝑢 ∈ 𝐸 , 𝑣 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑢 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		tendoplcbv.p	⊢ 𝑃 = ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
2		fveq1	⊢ ( 𝑠 = 𝑢 → ( 𝑠 ‘ 𝑓 ) = ( 𝑢 ‘ 𝑓 ) )
3	2	coeq1d	⊢ ( 𝑠 = 𝑢 → ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) = ( ( 𝑢 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) )
4	3	mpteq2dv	⊢ ( 𝑠 = 𝑢 → ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) = ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑢 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
5		fveq1	⊢ ( 𝑡 = 𝑣 → ( 𝑡 ‘ 𝑓 ) = ( 𝑣 ‘ 𝑓 ) )
6	5	coeq2d	⊢ ( 𝑡 = 𝑣 → ( ( 𝑢 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) = ( ( 𝑢 ‘ 𝑓 ) ∘ ( 𝑣 ‘ 𝑓 ) ) )
7	6	mpteq2dv	⊢ ( 𝑡 = 𝑣 → ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑢 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) = ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑢 ‘ 𝑓 ) ∘ ( 𝑣 ‘ 𝑓 ) ) ) )
8		fveq2	⊢ ( 𝑓 = 𝑔 → ( 𝑢 ‘ 𝑓 ) = ( 𝑢 ‘ 𝑔 ) )
9		fveq2	⊢ ( 𝑓 = 𝑔 → ( 𝑣 ‘ 𝑓 ) = ( 𝑣 ‘ 𝑔 ) )
10	8 9	coeq12d	⊢ ( 𝑓 = 𝑔 → ( ( 𝑢 ‘ 𝑓 ) ∘ ( 𝑣 ‘ 𝑓 ) ) = ( ( 𝑢 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) )
11	10	cbvmptv	⊢ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑢 ‘ 𝑓 ) ∘ ( 𝑣 ‘ 𝑓 ) ) ) = ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑢 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) )
12	7 11	eqtrdi	⊢ ( 𝑡 = 𝑣 → ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑢 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) = ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑢 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) ) )
13	4 12	cbvmpov	⊢ ( 𝑠 ∈ 𝐸 , 𝑡 ∈ 𝐸 ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) = ( 𝑢 ∈ 𝐸 , 𝑣 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑢 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) ) )
14	1 13	eqtri	⊢ 𝑃 = ( 𝑢 ∈ 𝐸 , 𝑣 ∈ 𝐸 ↦ ( 𝑔 ∈ 𝑇 ↦ ( ( 𝑢 ‘ 𝑔 ) ∘ ( 𝑣 ‘ 𝑔 ) ) ) )