Metamath Proof Explorer


Theorem hlmulf

Description: Mapping for Hilbert space scalar multiplication. (Contributed by NM, 7-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses hlmulf.1 X = BaseSet U
hlmulf.4 S = 𝑠OLD U
Assertion hlmulf U CHil OLD S : × X X

Proof

Step Hyp Ref Expression
1 hlmulf.1 X = BaseSet U
2 hlmulf.4 S = 𝑠OLD U
3 hlnv U CHil OLD U NrmCVec
4 1 2 nvsf U NrmCVec S : × X X
5 3 4 syl U CHil OLD S : × X X