Description: Mapping for the scalar multiplication operation. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nvsf.1 | |- X = ( BaseSet ` U ) |
|
| nvsf.4 | |- S = ( .sOLD ` U ) |
||
| Assertion | nvsf | |- ( U e. NrmCVec -> S : ( CC X. X ) --> X ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nvsf.1 | |- X = ( BaseSet ` U ) |
|
| 2 | nvsf.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 | vcsm | |- ( ( 1st ` U ) e. CVecOLD -> S : ( CC X. X ) --> X ) |
| 10 | 4 9 | syl | |- ( U e. NrmCVec -> S : ( CC X. X ) --> X ) |