norm0

Description: The norm of a zero vector. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

		Ref	Expression
	Assertion	norm0	$⊢ {norm}_{ℎ} (0_{ℎ}) = 0$

Step	Hyp	Ref	Expression
1		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
2		normval	$⊢ 0_{ℎ} \in ℋ \to {norm}_{ℎ} (0_{ℎ}) = \sqrt{0_{ℎ} \cdot_{ih} 0_{ℎ}}$
3	1 2	ax-mp	$⊢ {norm}_{ℎ} (0_{ℎ}) = \sqrt{0_{ℎ} \cdot_{ih} 0_{ℎ}}$
4		hi01	$⊢ 0_{ℎ} \in ℋ \to 0_{ℎ} \cdot_{ih} 0_{ℎ} = 0$
5	4	fveq2d	$⊢ 0_{ℎ} \in ℋ \to \sqrt{0_{ℎ} \cdot_{ih} 0_{ℎ}} = \sqrt{0}$
6	1 5	ax-mp	$⊢ \sqrt{0_{ℎ} \cdot_{ih} 0_{ℎ}} = \sqrt{0}$
7		sqrt0	$⊢ \sqrt{0} = 0$
8	3 6 7	3eqtri	$⊢ {norm}_{ℎ} (0_{ℎ}) = 0$

Metamath Proof Explorer