Theorem norm-i

Description: Theorem 3.3(i) of Beran p. 97. (Contributed by NM, 29-Jul-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	norm-i	⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ 𝐴 ) = 0 ↔ 𝐴 = 0ℎ ) )

Proof

Step	Hyp	Ref	Expression
1		normgt0	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ≠ 0ℎ ↔ 0 < ( normℎ ‘ 𝐴 ) ) )
2		normcl	⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ 𝐴 ) ∈ ℝ )
3		normge0	⊢ ( 𝐴 ∈ ℋ → 0 ≤ ( normℎ ‘ 𝐴 ) )
4		0re	⊢ 0 ∈ ℝ
5		leltne	⊢ ( ( 0 ∈ ℝ ∧ ( normℎ ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ 𝐴 ) ) → ( 0 < ( normℎ ‘ 𝐴 ) ↔ ( normℎ ‘ 𝐴 ) ≠ 0 ) )
6	4 5	mp3an1	⊢ ( ( ( normℎ ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ 𝐴 ) ) → ( 0 < ( normℎ ‘ 𝐴 ) ↔ ( normℎ ‘ 𝐴 ) ≠ 0 ) )
7	2 3 6	syl2anc	⊢ ( 𝐴 ∈ ℋ → ( 0 < ( normℎ ‘ 𝐴 ) ↔ ( normℎ ‘ 𝐴 ) ≠ 0 ) )
8	1 7	bitrd	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ≠ 0ℎ ↔ ( normℎ ‘ 𝐴 ) ≠ 0 ) )
9	8	necon4bid	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 = 0ℎ ↔ ( normℎ ‘ 𝐴 ) = 0 ) )
10	9	bicomd	⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ 𝐴 ) = 0 ↔ 𝐴 = 0ℎ ) )