Description: Closure law for the scalar product operation of a normed complex vector space. (Contributed by NM, 1-Feb-2007) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nvscl.1 | |- X = ( BaseSet ` U ) |
|
| nvscl.4 | |- S = ( .sOLD ` U ) |
||
| Assertion | nvscl | |- ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( A S B ) e. X ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nvscl.1 | |- X = ( BaseSet ` U ) |
|
| 2 | nvscl.4 | |- S = ( .sOLD ` U ) |
|
| 3 | eqid | |- ( 1st ` U ) = ( 1st ` U ) |
|
| 4 | 3 | nvvc | |- ( U e. NrmCVec -> ( 1st ` U ) e. CVecOLD ) |
| 5 | eqid | |- ( +v ` U ) = ( +v ` U ) |
|
| 6 | 5 | vafval | |- ( +v ` U ) = ( 1st ` ( 1st ` U ) ) |
| 7 | 2 | smfval | |- S = ( 2nd ` ( 1st ` U ) ) |
| 8 | 1 5 | bafval | |- X = ran ( +v ` U ) |
| 9 | 6 7 8 | vccl | |- ( ( ( 1st ` U ) e. CVecOLD /\ A e. CC /\ B e. X ) -> ( A S B ) e. X ) |
| 10 | 4 9 | syl3an1 | |- ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( A S B ) e. X ) |