Metamath Proof Explorer


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 )