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 = ( 1st ` W )
	vciOLD.2	|- S = ( 2nd ` W )
	vciOLD.3	|- X = ran G
Assertion	vccl	|- ( ( W e. CVecOLD /\ A e. CC /\ B e. X ) -> ( A S B ) e. X )

Proof

Step	Hyp	Ref	Expression
1		vciOLD.1	|- G = ( 1st ` W )
2		vciOLD.2	|- S = ( 2nd ` W )
3		vciOLD.3	|- X = ran G
4	1 2 3	vcsm	|- ( W e. CVecOLD -> S : ( CC X. X ) --> X )
5		fovrn	|- ( ( S : ( CC X. X ) --> X /\ A e. CC /\ B e. X ) -> ( A S B ) e. X )
6	4 5	syl3an1	|- ( ( W e. CVecOLD /\ A e. CC /\ B e. X ) -> ( A S B ) e. X )