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 f T s f -1
Assertion tendoicbv I = u E g T u g -1

Proof

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