This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ ℋ → ( 𝐴 ≠ 0ℎ ↔ 0 < ( normℎ ‘ 𝐴 ) ) )

Proof

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