Theorem normgt0

Description: The norm of nonzero vector is positive. (Contributed by NM, 10-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	normgt0	$$⊢A\in \mathscr{H}\to \left(A\ne 0_{ℎ}\leftrightarrow 0<{norm}_{ℎ}\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hiidrcl	$$⊢A\in \mathscr{H}\to A{\cdot }_{\mathrm{ih}}A\in ℝ$$
2	1	adantr	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to A{\cdot }_{\mathrm{ih}}A\in ℝ$$
3		ax-his4	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to 0<A{\cdot }_{\mathrm{ih}}A$$
4		sqrtgt0	$$⊢\left(A{\cdot }_{\mathrm{ih}}A\in ℝ\wedge 0<A{\cdot }_{\mathrm{ih}}A\right)\to 0<\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
5	2 3 4	syl2anc	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to 0<\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
6	5	ex	$$⊢A\in \mathscr{H}\to \left(A\ne 0_{ℎ}\to 0<\sqrt{A{\cdot }_{\mathrm{ih}}A}\right)$$
7		oveq1	$$⊢A=0_{ℎ}\to A{\cdot }_{\mathrm{ih}}A=0_{ℎ}{\cdot }_{\mathrm{ih}}A$$
8		hi01	$$⊢A\in \mathscr{H}\to 0_{ℎ}{\cdot }_{\mathrm{ih}}A=0$$
9	7 8	sylan9eqr	$$⊢\left(A\in \mathscr{H}\wedge A=0_{ℎ}\right)\to A{\cdot }_{\mathrm{ih}}A=0$$
10	9	fveq2d	$$⊢\left(A\in \mathscr{H}\wedge A=0_{ℎ}\right)\to \sqrt{A{\cdot }_{\mathrm{ih}}A}=\sqrt{0}$$
11		sqrt0	$$⊢\sqrt{0}=0$$
12	10 11	eqtrdi	$$⊢\left(A\in \mathscr{H}\wedge A=0_{ℎ}\right)\to \sqrt{A{\cdot }_{\mathrm{ih}}A}=0$$
13	12	ex	$$⊢A\in \mathscr{H}\to \left(A=0_{ℎ}\to \sqrt{A{\cdot }_{\mathrm{ih}}A}=0\right)$$
14		hiidge0	$$⊢A\in \mathscr{H}\to 0\le A{\cdot }_{\mathrm{ih}}A$$
15	1 14	resqrtcld	$$⊢A\in \mathscr{H}\to \sqrt{A{\cdot }_{\mathrm{ih}}A}\in ℝ$$
16		0re	$$⊢0\in ℝ$$
17		lttri3	$$⊢\left(\sqrt{A{\cdot }_{\mathrm{ih}}A}\in ℝ\wedge 0\in ℝ\right)\to \left(\sqrt{A{\cdot }_{\mathrm{ih}}A}=0\leftrightarrow \left(\neg \sqrt{A{\cdot }_{\mathrm{ih}}A}<0\wedge \neg 0<\sqrt{A{\cdot }_{\mathrm{ih}}A}\right)\right)$$
18	15 16 17	sylancl	$$⊢A\in \mathscr{H}\to \left(\sqrt{A{\cdot }_{\mathrm{ih}}A}=0\leftrightarrow \left(\neg \sqrt{A{\cdot }_{\mathrm{ih}}A}<0\wedge \neg 0<\sqrt{A{\cdot }_{\mathrm{ih}}A}\right)\right)$$
19		simpr	$$⊢\left(\neg \sqrt{A{\cdot }_{\mathrm{ih}}A}<0\wedge \neg 0<\sqrt{A{\cdot }_{\mathrm{ih}}A}\right)\to \neg 0<\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
20	18 19	syl6bi	$$⊢A\in \mathscr{H}\to \left(\sqrt{A{\cdot }_{\mathrm{ih}}A}=0\to \neg 0<\sqrt{A{\cdot }_{\mathrm{ih}}A}\right)$$
21	13 20	syld	$$⊢A\in \mathscr{H}\to \left(A=0_{ℎ}\to \neg 0<\sqrt{A{\cdot }_{\mathrm{ih}}A}\right)$$
22	21	necon2ad	$$⊢A\in \mathscr{H}\to \left(0<\sqrt{A{\cdot }_{\mathrm{ih}}A}\to A\ne 0_{ℎ}\right)$$
23	6 22	impbid	$$⊢A\in \mathscr{H}\to \left(A\ne 0_{ℎ}\leftrightarrow 0<\sqrt{A{\cdot }_{\mathrm{ih}}A}\right)$$
24		normval	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(A\right)=\sqrt{A{\cdot }_{\mathrm{ih}}A}$$
25	24	breq2d	$$⊢A\in \mathscr{H}\to \left(0<{norm}_{ℎ}\left(A\right)\leftrightarrow 0<\sqrt{A{\cdot }_{\mathrm{ih}}A}\right)$$
26	23 25	bitr4d	$$⊢A\in \mathscr{H}\to \left(A\ne 0_{ℎ}\leftrightarrow 0<{norm}_{ℎ}\left(A\right)\right)$$