Theorem normge0

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

	Ref	Expression
Assertion	normge0	$$⊢A\in \mathscr{H}\to 0\le {norm}_{ℎ}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		hiidrcl	$$⊢A\in \mathscr{H}\to A{\cdot }_{\mathrm{ih}}A\in ℝ$$
2		hiidge0	$$⊢A\in \mathscr{H}\to 0\le A{\cdot }_{\mathrm{ih}}A$$
3	1 2	sqrtge0d	$$⊢A\in \mathscr{H}\to 0\le \sqrt{A{\cdot }_{\mathrm{ih}}A}$$
4		normval	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(A\right)=\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
5	3 4	breqtrrd	$$⊢A\in \mathscr{H}\to 0\le {norm}_{ℎ}\left(A\right)$$