This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ X = BaseSet ⁡ U
nvsf.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
Assertion nvsf ⊢ U ∈ NrmCVec → S : ℂ × X ⟶ X

Proof

Step Hyp Ref Expression
1 nvsf.1 ⊢ X = BaseSet ⁡ U
2 nvsf.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
3 eqid ⊢ 1 st ⁡ U = 1 st ⁡ U
4 3 nvvc ⊢ U ∈ NrmCVec → 1 st ⁡ U ∈ CVec OLD
5 eqid ⊢ + v ⁡ U = + v ⁡ U
6 5 vafval ⊢ + v ⁡ U = 1 st ⁡ 1 st ⁡ U
7 2 smfval ⊢ S = 2 nd ⁡ 1 st ⁡ U
8 1 5 bafval ⊢ X = ran ⁡ + v ⁡ U
9 6 7 8 vcsm ⊢ 1 st ⁡ U ∈ CVec OLD → S : ℂ × X ⟶ X
10 4 9 syl ⊢ U ∈ NrmCVec → S : ℂ × X ⟶ X