Theorem hhba

Description: The base set of Hilbert space. This theorem provides an independent proof of df-hba (see comments in that definition). (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhnv.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
Assertion	hhba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		hilablo	$$⊢{+}_{ℎ}\in \mathrm{AbelOp}$$
3		ablogrpo	$$⊢{+}_{ℎ}\in \mathrm{AbelOp}\to {+}_{ℎ}\in \mathrm{GrpOp}$$
4	2 3	ax-mp	$$⊢{+}_{ℎ}\in \mathrm{GrpOp}$$
5		ax-hfvadd	$$⊢{+}_{ℎ}:\mathscr{H}\times \mathscr{H}⟶\mathscr{H}$$
6	5	fdmi	$$⊢\mathrm{dom}{+}_{ℎ}=\mathscr{H}\times \mathscr{H}$$
7	4 6	grporn	$$⊢\mathscr{H}=\mathrm{ran}{+}_{ℎ}$$
8		eqid	$$⊢\mathrm{BaseSet}\left(U\right)=\mathrm{BaseSet}\left(U\right)$$
9	1	hhva	$$⊢{+}_{ℎ}={+}_v\left(U\right)$$
10	8 9	bafval	$$⊢\mathrm{BaseSet}\left(U\right)=\mathrm{ran}{+}_{ℎ}$$
11	7 10	eqtr4i	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$