Theorem tendospcl

Description: Closure of endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013)

	Ref	Expression
Hypotheses	tendosp.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	tendosp.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	tendosp.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
Assertion	tendospcl	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge U\in E\wedge F\in T\right)\to U\left(F\right)\in T$$

Proof

Step	Hyp	Ref	Expression
1		tendosp.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		tendosp.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
3		tendosp.e	$$⊢E=\mathrm{TEndo}\left(K\right)\left(W\right)$$
4	1 2 3	tendocl	$$⊢\left(\left(K\in V\wedge W\in H\right)\wedge U\in E\wedge F\in T\right)\to U\left(F\right)\in T$$