Theorem vccl

Description: Closure of the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vciOLD.1	$$⊢G=1^{st}\left(W\right)$$
	vciOLD.2	$$⊢S=2^{nd}\left(W\right)$$
	vciOLD.3	$$⊢X=\mathrm{ran}G$$
Assertion	vccl	$$⊢\left(W\in {CVec}_{\mathrm{OLD}}\wedge A\in ℂ\wedge B\in X\right)\to ASB\in X$$

Proof

Step	Hyp	Ref	Expression
1		vciOLD.1	$$⊢G=1^{st}\left(W\right)$$
2		vciOLD.2	$$⊢S=2^{nd}\left(W\right)$$
3		vciOLD.3	$$⊢X=\mathrm{ran}G$$
4	1 2 3	vcsm	$$⊢W\in {CVec}_{\mathrm{OLD}}\to S:ℂ\times X⟶X$$
5		fovcdm	$$⊢\left(S:ℂ\times X⟶X\wedge A\in ℂ\wedge B\in X\right)\to ASB\in X$$
6	4 5	syl3an1	$$⊢\left(W\in {CVec}_{\mathrm{OLD}}\wedge A\in ℂ\wedge B\in X\right)\to ASB\in X$$