dfhnorm2

Description: Alternate definition of the norm of a vector of Hilbert space. Definition of norm in Beran p. 96. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	dfhnorm2	$⊢ {norm}_{ℎ} = (x \in ℋ ⟼ \sqrt{x \cdot_{ih} x})$

Proof

Step	Hyp	Ref	Expression
1		df-hnorm	$⊢ {norm}_{ℎ} = (x \in dom dom \cdot_{ih} ⟼ \sqrt{x \cdot_{ih} x})$
2		ax-hfi	$⊢ \cdot_{ih} : ℋ \times ℋ ⟶ ℂ$
3	2	fdmi	$⊢ dom \cdot_{ih} = ℋ \times ℋ$
4	3	dmeqi	$⊢ dom dom \cdot_{ih} = dom (ℋ \times ℋ)$
5		dmxpid	$⊢ dom (ℋ \times ℋ) = ℋ$
6	4 5	eqtr2i	$⊢ ℋ = dom dom \cdot_{ih}$
7	6	mpteq1i	$⊢ (x \in ℋ ⟼ \sqrt{x \cdot_{ih} x}) = (x \in dom dom \cdot_{ih} ⟼ \sqrt{x \cdot_{ih} x})$
8	1 7	eqtr4i	$⊢ {norm}_{ℎ} = (x \in ℋ ⟼ \sqrt{x \cdot_{ih} x})$

Metamath Proof Explorer

Theorem dfhnorm2

Proof