Metamath Proof Explorer

Theorem nvsf

Description: Mapping for the scalar multiplication operation. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvsf.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
nvsf.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
Assertion nvsf ( ๐‘ˆ โˆˆ NrmCVec โ†’ ๐‘† : ( โ„‚ ร— ๐‘‹ ) โŸถ ๐‘‹ )

Proof

Step Hyp Ref Expression
1 nvsf.1 โŠข ๐‘‹ = ( BaseSet โ€˜ ๐‘ˆ )
2 nvsf.4 โŠข ๐‘† = ( ยท๐‘ OLD โ€˜ ๐‘ˆ )
3 eqid โŠข ( 1st โ€˜ ๐‘ˆ ) = ( 1st โ€˜ ๐‘ˆ )
4 3 nvvc โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ( 1st โ€˜ ๐‘ˆ ) โˆˆ CVecOLD )
5 eqid โŠข ( +๐‘ฃ โ€˜ ๐‘ˆ ) = ( +๐‘ฃ โ€˜ ๐‘ˆ )
6 5 vafval โŠข ( +๐‘ฃ โ€˜ ๐‘ˆ ) = ( 1st โ€˜ ( 1st โ€˜ ๐‘ˆ ) )
7 2 smfval โŠข ๐‘† = ( 2nd โ€˜ ( 1st โ€˜ ๐‘ˆ ) )
8 1 5 bafval โŠข ๐‘‹ = ran ( +๐‘ฃ โ€˜ ๐‘ˆ )
9 6 7 8 vcsm โŠข ( ( 1st โ€˜ ๐‘ˆ ) โˆˆ CVecOLD โ†’ ๐‘† : ( โ„‚ ร— ๐‘‹ ) โŸถ ๐‘‹ )
10 4 9 syl โŠข ( ๐‘ˆ โˆˆ NrmCVec โ†’ ๐‘† : ( โ„‚ ร— ๐‘‹ ) โŸถ ๐‘‹ )