Metamath Proof Explorer


Theorem hhsm

Description: The scalar product operation of Hilbert space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypothesis hhnv.1 U = + norm
Assertion hhsm = 𝑠OLD U

Proof

Step Hyp Ref Expression
1 hhnv.1 U = + norm
2 1 hhnv U NrmCVec
3 1 2 h2hsm = 𝑠OLD U