This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ( s e. E , t e. E \|-> ( f e. T \|-> ( ( s ` f ) o. ( t ` f ) ) ) )
	Assertion	tendoplcbv	\|- P = ( u e. E , v e. E \|-> ( g e. T \|-> ( ( u ` g ) o. ( v ` g ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		tendoplcbv.p	\|- P = ( s e. E , t e. E \|-> ( f e. T \|-> ( ( s ` f ) o. ( t ` f ) ) ) )
2		fveq1	\|- ( s = u -> ( s ` f ) = ( u ` f ) )
3	2	coeq1d	\|- ( s = u -> ( ( s ` f ) o. ( t ` f ) ) = ( ( u ` f ) o. ( t ` f ) ) )
4	3	mpteq2dv	\|- ( s = u -> ( f e. T \|-> ( ( s ` f ) o. ( t ` f ) ) ) = ( f e. T \|-> ( ( u ` f ) o. ( t ` f ) ) ) )
5		fveq1	\|- ( t = v -> ( t ` f ) = ( v ` f ) )
6	5	coeq2d	\|- ( t = v -> ( ( u ` f ) o. ( t ` f ) ) = ( ( u ` f ) o. ( v ` f ) ) )
7	6	mpteq2dv	\|- ( t = v -> ( f e. T \|-> ( ( u ` f ) o. ( t ` f ) ) ) = ( f e. T \|-> ( ( u ` f ) o. ( v ` f ) ) ) )
8		fveq2	\|- ( f = g -> ( u ` f ) = ( u ` g ) )
9		fveq2	\|- ( f = g -> ( v ` f ) = ( v ` g ) )
10	8 9	coeq12d	\|- ( f = g -> ( ( u ` f ) o. ( v ` f ) ) = ( ( u ` g ) o. ( v ` g ) ) )
11	10	cbvmptv	\|- ( f e. T \|-> ( ( u ` f ) o. ( v ` f ) ) ) = ( g e. T \|-> ( ( u ` g ) o. ( v ` g ) ) )
12	7 11	eqtrdi	\|- ( t = v -> ( f e. T \|-> ( ( u ` f ) o. ( t ` f ) ) ) = ( g e. T \|-> ( ( u ` g ) o. ( v ` g ) ) ) )
13	4 12	cbvmpov	\|- ( s e. E , t e. E \|-> ( f e. T \|-> ( ( s ` f ) o. ( t ` f ) ) ) ) = ( u e. E , v e. E \|-> ( g e. T \|-> ( ( u ` g ) o. ( v ` g ) ) ) )
14	1 13	eqtri	\|- P = ( u e. E , v e. E \|-> ( g e. T \|-> ( ( u ` g ) o. ( v ` g ) ) ) )