Theorem norm0

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

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

Proof

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