Theorem hhva

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

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

Proof

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