Theorem hhnv

Description: Hilbert space is a normed complex vector space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhnv.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
Assertion	hhnv	$$⊢U\in \mathrm{NrmCVec}$$

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		hilid	$$⊢\mathrm{GId}\left({+}_{ℎ}\right)=0_{ℎ}$$
9	8	eqcomi	$$⊢0_{ℎ}=\mathrm{GId}\left({+}_{ℎ}\right)$$
10		hilvc	$$⊢⟨{+}_{ℎ},{\cdot }_{ℎ}⟩\in {CVec}_{\mathrm{OLD}}$$
11		normf	$$⊢{norm}_{ℎ}:\mathscr{H}⟶ℝ$$
12		norm-i	$$⊢x\in \mathscr{H}\to \left({norm}_{ℎ}\left(x\right)=0\leftrightarrow x=0_{ℎ}\right)$$
13	12	biimpa	$$⊢\left(x\in \mathscr{H}\wedge {norm}_{ℎ}\left(x\right)=0\right)\to x=0_{ℎ}$$
14		norm-iii	$$⊢\left(y\in ℂ\wedge x\in \mathscr{H}\right)\to {norm}_{ℎ}\left(y{\cdot }_{ℎ}x\right)=\left|y\right|{norm}_{ℎ}\left(x\right)$$
15		norm-ii	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to {norm}_{ℎ}\left(x{+}_{ℎ}y\right)\le {norm}_{ℎ}\left(x\right)+{norm}_{ℎ}\left(y\right)$$
16	7 9 10 11 13 14 15 1	isnvi	$$⊢U\in \mathrm{NrmCVec}$$