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	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
	hilhh.2	$$⊢{+}_{ℎ}={+}_v\left(U\right)$$
	hilhh.3	$$⊢{\cdot }_{ℎ}={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
	hilhh.5	$$⊢{\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
	hilhh.9	$$⊢U\in \mathrm{NrmCVec}$$
Assertion	hilhhi	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$

Proof

Step	Hyp	Ref	Expression
1		hilhh.1	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
2		hilhh.2	$$⊢{+}_{ℎ}={+}_v\left(U\right)$$
3		hilhh.3	$$⊢{\cdot }_{ℎ}={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
4		hilhh.5	$$⊢{\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
5		hilhh.9	$$⊢U\in \mathrm{NrmCVec}$$
6	1 4 5	hilnormi	$$⊢{norm}_{ℎ}={norm}_{CV}\left(U\right)$$
7	2 3 6	nvop	$$⊢U\in \mathrm{NrmCVec}\to U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
8	5 7	ax-mp	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$