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

Metamath Proof Explorer

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