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	syl6bi	⊢ ( 𝐴 ∈ ℋ → ( ( √ ‘ ( 𝐴 ·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ℎ ‘ 𝐴 ) ) )