This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hhnm

Description: The norm function of Hilbert space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	hhnv.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
	Assertion	hhnm	$⊢ {norm}_{ℎ} = {norm}_{CV} (U)$

Step	Hyp	Ref	Expression
1		hhnv.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
2	1	hhnv	$⊢ U \in NrmCVec$
3	1 2	h2hnm	$⊢ {norm}_{ℎ} = {norm}_{CV} (U)$