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 NrmCVec$

Step	Hyp	Ref	Expression
1		hhnv.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
2		hilablo	$⊢ +_{ℎ} \in AbelOp$
3		ablogrpo	$⊢ +_{ℎ} \in AbelOp \to +_{ℎ} \in GrpOp$
4	2 3	ax-mp	$⊢ +_{ℎ} \in GrpOp$
5		ax-hfvadd	$⊢ +_{ℎ} : ℋ \times ℋ ⟶ ℋ$
6	5	fdmi	$⊢ dom +_{ℎ} = ℋ \times ℋ$
7	4 6	grporn	$⊢ ℋ = ran +_{ℎ}$
8		hilid	$⊢ GId (+_{ℎ}) = 0_{ℎ}$
9	8	eqcomi	$⊢ 0_{ℎ} = GId (+_{ℎ})$
10		hilvc	$⊢ ⟨+_{ℎ}, \cdot_{ℎ}⟩ \in {CVec}_{OLD}$
11		normf	$⊢ {norm}_{ℎ} : ℋ ⟶ ℝ$
12		norm-i	$⊢ x \in ℋ \to ({norm}_{ℎ} (x) = 0 \leftrightarrow x = 0_{ℎ})$
13	12	biimpa	$⊢ (x \in ℋ \land {norm}_{ℎ} (x) = 0) \to x = 0_{ℎ}$
14		norm-iii	$⊢ (y \in ℂ \land x \in ℋ) \to {norm}_{ℎ} (y \cdot_{ℎ} x) = \|y\| {norm}_{ℎ} (x)$
15		norm-ii	$⊢ (x \in ℋ \land y \in ℋ) \to {norm}_{ℎ} (x +_{ℎ} y) \leq {norm}_{ℎ} (x) + {norm}_{ℎ} (y)$
16	7 9 10 11 13 14 15 1	isnvi	$⊢ U \in NrmCVec$

Metamath Proof Explorer