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