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 ) |
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 ) |