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 ∈ ℋ → A ≠ 0 ℎ ↔ 0 < norm ℎ ⁡ A

Proof

Step Hyp Ref Expression
1 hiidrcl ⊢ A ∈ ℋ → A ⋅ ih A ∈ ℝ
2 1 adantr ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → A ⋅ ih A ∈ ℝ
3 ax-his4 ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 < A ⋅ ih A
4 sqrtgt0 ⊢ A ⋅ ih A ∈ ℝ ∧ 0 < A ⋅ ih A → 0 < A ⋅ ih A
5 2 3 4 syl2anc ⊢ A ∈ ℋ ∧ A ≠ 0 ℎ → 0 < A ⋅ ih A
6 5 ex ⊢ A ∈ ℋ → A ≠ 0 ℎ → 0 < A ⋅ ih A
7 oveq1 ⊢ A = 0 ℎ → A ⋅ ih A = 0 ℎ ⋅ ih A
8 hi01 ⊢ A ∈ ℋ → 0 ℎ ⋅ ih A = 0
9 7 8 sylan9eqr ⊢ A ∈ ℋ ∧ A = 0 ℎ → A ⋅ ih A = 0
10 9 fveq2d ⊢ A ∈ ℋ ∧ A = 0 ℎ → A ⋅ ih A = 0
11 sqrt0 ⊢ 0 = 0
12 10 11 eqtrdi ⊢ A ∈ ℋ ∧ A = 0 ℎ → A ⋅ ih A = 0
13 12 ex ⊢ A ∈ ℋ → A = 0 ℎ → A ⋅ ih A = 0
14 hiidge0 ⊢ A ∈ ℋ → 0 ≤ A ⋅ ih A
15 1 14 resqrtcld ⊢ A ∈ ℋ → A ⋅ ih A ∈ ℝ
16 0re ⊢ 0 ∈ ℝ
17 lttri3 ⊢ A ⋅ ih A ∈ ℝ ∧ 0 ∈ ℝ → A ⋅ ih A = 0 ↔ ¬ A ⋅ ih A < 0 ∧ ¬ 0 < A ⋅ ih A
18 15 16 17 sylancl ⊢ A ∈ ℋ → A ⋅ ih A = 0 ↔ ¬ A ⋅ ih A < 0 ∧ ¬ 0 < A ⋅ ih A
19 simpr ⊢ ¬ A ⋅ ih A < 0 ∧ ¬ 0 < A ⋅ ih A → ¬ 0 < A ⋅ ih A
20 18 19 biimtrdi ⊢ A ∈ ℋ → A ⋅ ih A = 0 → ¬ 0 < A ⋅ ih A
21 13 20 syld ⊢ A ∈ ℋ → A = 0 ℎ → ¬ 0 < A ⋅ ih A
22 21 necon2ad ⊢ A ∈ ℋ → 0 < A ⋅ ih A → A ≠ 0 ℎ
23 6 22 impbid ⊢ A ∈ ℋ → A ≠ 0 ℎ ↔ 0 < A ⋅ ih A
24 normval ⊢ A ∈ ℋ → norm ℎ ⁡ A = A ⋅ ih A
25 24 breq2d ⊢ A ∈ ℋ → 0 < norm ℎ ⁡ A ↔ 0 < A ⋅ ih A
26 23 25 bitr4d ⊢ A ∈ ℋ → A ≠ 0 ℎ ↔ 0 < norm ℎ ⁡ A