Theorem vcsm

Description: Functionality of th 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	vcsm	$$⊢W\in {CVec}_{\mathrm{OLD}}\to S:ℂ\times X⟶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	vciOLD	$$⊢W\in {CVec}_{\mathrm{OLD}}\to \left(G\in \mathrm{AbelOp}\wedge S:ℂ\times X⟶X\wedge \forall x\in X\left(1Sx=x\wedge \forall y\in ℂ\left(\forall z\in XyS\left(xGz\right)=\left(ySx\right)G\left(ySz\right)\wedge \forall z\in ℂ\left(\left(y+z\right)Sx=\left(ySx\right)G\left(zSx\right)\wedge yzSx=yS\left(zSx\right)\right)\right)\right)\right)$$
5	4	simp2d	$$⊢W\in {CVec}_{\mathrm{OLD}}\to S:ℂ\times X⟶X$$