Theorem hhvs

Description: The vector subtraction operation of Hilbert space. (Contributed by NM, 13-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
Assertion	hhvs	⊢ −ℎ = ( −𝑣 ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2	1	hhnv	⊢ 𝑈 ∈ NrmCVec
3	1	hhba	⊢ ℋ = ( BaseSet ‘ 𝑈 )
4	1 2 3	h2hvs	⊢ −ℎ = ( −𝑣 ‘ 𝑈 )