# Metamath Proof Explorer

## 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 ℋ\to \left({A}\ne {0}_{ℎ}↔0<{norm}_{ℎ}\left({A}\right)\right)$

### Proof

Step Hyp Ref Expression
1 hiidrcl ${⊢}{A}\in ℋ\to {A}{\cdot }_{\mathrm{ih}}{A}\in ℝ$
2 1 adantr ${⊢}\left({A}\in ℋ\wedge {A}\ne {0}_{ℎ}\right)\to {A}{\cdot }_{\mathrm{ih}}{A}\in ℝ$
3 ax-his4 ${⊢}\left({A}\in ℋ\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 ℋ\wedge {A}\ne {0}_{ℎ}\right)\to 0<\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}$
6 5 ex ${⊢}{A}\in ℋ\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 ℋ\to {0}_{ℎ}{\cdot }_{\mathrm{ih}}{A}=0$
9 7 8 sylan9eqr ${⊢}\left({A}\in ℋ\wedge {A}={0}_{ℎ}\right)\to {A}{\cdot }_{\mathrm{ih}}{A}=0$
10 9 fveq2d ${⊢}\left({A}\in ℋ\wedge {A}={0}_{ℎ}\right)\to \sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}=\sqrt{0}$
11 sqrt0 ${⊢}\sqrt{0}=0$
12 10 11 syl6eq ${⊢}\left({A}\in ℋ\wedge {A}={0}_{ℎ}\right)\to \sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}=0$
13 12 ex ${⊢}{A}\in ℋ\to \left({A}={0}_{ℎ}\to \sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}=0\right)$
14 hiidge0 ${⊢}{A}\in ℋ\to 0\le {A}{\cdot }_{\mathrm{ih}}{A}$
15 1 14 resqrtcld ${⊢}{A}\in ℋ\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↔\left(¬\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}<0\wedge ¬0<\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}\right)\right)$
18 15 16 17 sylancl ${⊢}{A}\in ℋ\to \left(\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}=0↔\left(¬\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}<0\wedge ¬0<\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}\right)\right)$
19 simpr ${⊢}\left(¬\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}<0\wedge ¬0<\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}\right)\to ¬0<\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}$
20 18 19 syl6bi ${⊢}{A}\in ℋ\to \left(\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}=0\to ¬0<\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}\right)$
21 13 20 syld ${⊢}{A}\in ℋ\to \left({A}={0}_{ℎ}\to ¬0<\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}\right)$
22 21 necon2ad ${⊢}{A}\in ℋ\to \left(0<\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}\to {A}\ne {0}_{ℎ}\right)$
23 6 22 impbid ${⊢}{A}\in ℋ\to \left({A}\ne {0}_{ℎ}↔0<\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}\right)$
24 normval ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({A}\right)=\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}$
25 24 breq2d ${⊢}{A}\in ℋ\to \left(0<{norm}_{ℎ}\left({A}\right)↔0<\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}\right)$
26 23 25 bitr4d ${⊢}{A}\in ℋ\to \left({A}\ne {0}_{ℎ}↔0<{norm}_{ℎ}\left({A}\right)\right)$