Theorem hilhhi

Description: Deduce the structure of Hilbert space from its components. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hilhh.1	⊢ ℋ = ( BaseSet ‘ 𝑈 )
	hilhh.2	⊢ +ℎ = ( +𝑣 ‘ 𝑈 )
	hilhh.3	⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )
	hilhh.5	⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 )
	hilhh.9	⊢ 𝑈 ∈ NrmCVec
Assertion	hilhhi	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩

Proof

Step	Hyp	Ref	Expression
1		hilhh.1	⊢ ℋ = ( BaseSet ‘ 𝑈 )
2		hilhh.2	⊢ +ℎ = ( +𝑣 ‘ 𝑈 )
3		hilhh.3	⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )
4		hilhh.5	⊢ ·ih = ( ·𝑖OLD ‘ 𝑈 )
5		hilhh.9	⊢ 𝑈 ∈ NrmCVec
6	1 4 5	hilnormi	⊢ normℎ = ( normCV ‘ 𝑈 )
7	2 3 6	nvop	⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
8	5 7	ax-mp	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩