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 → 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 )