Theorem tendoi2

Description: Value of additive 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	tendoi2	$$⊢\left(S\in E\wedge F\in T\right)\to I\left(S\right)\left(F\right)={S\left(F\right)}^{-1}$$

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	1 2	tendoi	$$⊢S\in E\to I\left(S\right)=\left(g\in T⟼{S\left(g\right)}^{-1}\right)$$
4	3	adantr	$$⊢\left(S\in E\wedge F\in T\right)\to I\left(S\right)=\left(g\in T⟼{S\left(g\right)}^{-1}\right)$$
5		fveq2	$$⊢g=F\to S\left(g\right)=S\left(F\right)$$
6	5	cnveqd	$$⊢g=F\to {S\left(g\right)}^{-1}={S\left(F\right)}^{-1}$$
7	6	adantl	$$⊢\left(\left(S\in E\wedge F\in T\right)\wedge g=F\right)\to {S\left(g\right)}^{-1}={S\left(F\right)}^{-1}$$
8		simpr	$$⊢\left(S\in E\wedge F\in T\right)\to F\in T$$
9		fvex	$$⊢S\left(F\right)\in \mathrm{V}$$
10	9	cnvex	$$⊢{S\left(F\right)}^{-1}\in \mathrm{V}$$
11	10	a1i	$$⊢\left(S\in E\wedge F\in T\right)\to {S\left(F\right)}^{-1}\in \mathrm{V}$$
12	4 7 8 11	fvmptd	$$⊢\left(S\in E\wedge F\in T\right)\to I\left(S\right)\left(F\right)={S\left(F\right)}^{-1}$$