Theorem tendoi

Description: Value of inverse endomorphism. (Contributed by NM, 12-Jun-2013)

	Ref	Expression
Hypotheses	tendoi.i	$$⊢I=\left(s\in E⟼\left(f\in T⟼{s\left(f\right)}^{-1}\right)\right)$$
	tendoi.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
Assertion	tendoi	$$⊢S\in E\to I\left(S\right)=\left(g\in T⟼{S\left(g\right)}^{-1}\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		tendoi.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		fveq1	$$⊢u=S\to u\left(g\right)=S\left(g\right)$$
4	3	cnveqd	$$⊢u=S\to {u\left(g\right)}^{-1}={S\left(g\right)}^{-1}$$
5	4	mpteq2dv	$$⊢u=S\to \left(g\in T⟼{u\left(g\right)}^{-1}\right)=\left(g\in T⟼{S\left(g\right)}^{-1}\right)$$
6	1	tendoicbv	$$⊢I=\left(u\in E⟼\left(g\in T⟼{u\left(g\right)}^{-1}\right)\right)$$
7	5 6 2	mptfvmpt	$$⊢S\in E\to I\left(S\right)=\left(g\in T⟼{S\left(g\right)}^{-1}\right)$$