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	$$⊢P=\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)$$
Assertion	tendoplcbv	$$⊢P=\left(u\in E,v\in E⟼\left(g\in T⟼u\left(g\right)\circ v\left(g\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		tendoplcbv.p	$$⊢P=\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)$$
2		fveq1	$$⊢s=u\to s\left(f\right)=u\left(f\right)$$
3	2	coeq1d	$$⊢s=u\to s\left(f\right)\circ t\left(f\right)=u\left(f\right)\circ t\left(f\right)$$
4	3	mpteq2dv	$$⊢s=u\to \left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)=\left(f\in T⟼u\left(f\right)\circ t\left(f\right)\right)$$
5		fveq1	$$⊢t=v\to t\left(f\right)=v\left(f\right)$$
6	5	coeq2d	$$⊢t=v\to u\left(f\right)\circ t\left(f\right)=u\left(f\right)\circ v\left(f\right)$$
7	6	mpteq2dv	$$⊢t=v\to \left(f\in T⟼u\left(f\right)\circ t\left(f\right)\right)=\left(f\in T⟼u\left(f\right)\circ v\left(f\right)\right)$$
8		fveq2	$$⊢f=g\to u\left(f\right)=u\left(g\right)$$
9		fveq2	$$⊢f=g\to v\left(f\right)=v\left(g\right)$$
10	8 9	coeq12d	$$⊢f=g\to u\left(f\right)\circ v\left(f\right)=u\left(g\right)\circ v\left(g\right)$$
11	10	cbvmptv	$$⊢\left(f\in T⟼u\left(f\right)\circ v\left(f\right)\right)=\left(g\in T⟼u\left(g\right)\circ v\left(g\right)\right)$$
12	7 11	eqtrdi	$$⊢t=v\to \left(f\in T⟼u\left(f\right)\circ t\left(f\right)\right)=\left(g\in T⟼u\left(g\right)\circ v\left(g\right)\right)$$
13	4 12	cbvmpov	$$⊢\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)=\left(u\in E,v\in E⟼\left(g\in T⟼u\left(g\right)\circ v\left(g\right)\right)\right)$$
14	1 13	eqtri	$$⊢P=\left(u\in E,v\in E⟼\left(g\in T⟼u\left(g\right)\circ v\left(g\right)\right)\right)$$