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 ) ) ) )