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=\left(s\in E⟼\left(f\in T⟼{s\left(f\right)}^{-1}\right)\right)$$
Assertion	tendoicbv	$$⊢I=\left(u\in E⟼\left(g\in T⟼{u\left(g\right)}^{-1}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		tendoi.i	$$⊢I=\left(s\in E⟼\left(f\in T⟼{s\left(f\right)}^{-1}\right)\right)$$
2		fveq1	$$⊢s=u\to s\left(f\right)=u\left(f\right)$$
3	2	cnveqd	$$⊢s=u\to {s\left(f\right)}^{-1}={u\left(f\right)}^{-1}$$
4	3	mpteq2dv	$$⊢s=u\to \left(f\in T⟼{s\left(f\right)}^{-1}\right)=\left(f\in T⟼{u\left(f\right)}^{-1}\right)$$
5		fveq2	$$⊢f=g\to u\left(f\right)=u\left(g\right)$$
6	5	cnveqd	$$⊢f=g\to {u\left(f\right)}^{-1}={u\left(g\right)}^{-1}$$
7	6	cbvmptv	$$⊢\left(f\in T⟼{u\left(f\right)}^{-1}\right)=\left(g\in T⟼{u\left(g\right)}^{-1}\right)$$
8	4 7	eqtrdi	$$⊢s=u\to \left(f\in T⟼{s\left(f\right)}^{-1}\right)=\left(g\in T⟼{u\left(g\right)}^{-1}\right)$$
9	8	cbvmptv	$$⊢\left(s\in E⟼\left(f\in T⟼{s\left(f\right)}^{-1}\right)\right)=\left(u\in E⟼\left(g\in T⟼{u\left(g\right)}^{-1}\right)\right)$$
10	1 9	eqtri	$$⊢I=\left(u\in E⟼\left(g\in T⟼{u\left(g\right)}^{-1}\right)\right)$$