Theorem tendoicbv

Description: Define inverse function for trace-preserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 12-Jun-2013)

	Ref	Expression
Hypothesis	tendoi.i	|- I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) )
Assertion	tendoicbv	|- I = ( u e. E |-> ( g e. T |-> `' ( u ` g ) ) )

Proof

Step	Hyp	Ref	Expression
1		tendoi.i	|- I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) )
2		fveq1	|- ( s = u -> ( s ` f ) = ( u ` f ) )
3	2	cnveqd	|- ( s = u -> `' ( s ` f ) = `' ( u ` f ) )
4	3	mpteq2dv	|- ( s = u -> ( f e. T |-> `' ( s ` f ) ) = ( f e. T |-> `' ( u ` f ) ) )
5		fveq2	|- ( f = g -> ( u ` f ) = ( u ` g ) )
6	5	cnveqd	|- ( f = g -> `' ( u ` f ) = `' ( u ` g ) )
7	6	cbvmptv	|- ( f e. T |-> `' ( u ` f ) ) = ( g e. T |-> `' ( u ` g ) )
8	4 7	eqtrdi	|- ( s = u -> ( f e. T |-> `' ( s ` f ) ) = ( g e. T |-> `' ( u ` g ) ) )
9	8	cbvmptv	|- ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) ) = ( u e. E |-> ( g e. T |-> `' ( u ` g ) ) )
10	1 9	eqtri	|- I = ( u e. E |-> ( g e. T |-> `' ( u ` g ) ) )