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	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
Assertion	hhsm	⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2	1	hhnv	⊢ 𝑈 ∈ NrmCVec
3	1 2	h2hsm	⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )