Theorem tendospdi2

Description: Reverse distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013)

	Ref	Expression
Hypotheses	tendospd.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	tendosp.p	$$⊢P=\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)$$
Assertion	tendospdi2	$$⊢\left(U\in E\wedge V\in E\wedge F\in T\right)\to \left(UPV\right)\left(F\right)=U\left(F\right)\circ V\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		tendospd.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
2		tendosp.p	$$⊢P=\left(s\in E,t\in E⟼\left(f\in T⟼s\left(f\right)\circ t\left(f\right)\right)\right)$$
3	2 1	tendopl2	$$⊢\left(U\in E\wedge V\in E\wedge F\in T\right)\to \left(UPV\right)\left(F\right)=U\left(F\right)\circ V\left(F\right)$$