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

Metamath Proof Explorer

Theorem norm-i-i

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

Ref Expression
Hypothesis normcl.1 ⊢ A ∈ ℋ
Assertion norm-i-i ⊢ norm ℎ ⁡ A = 0 ↔ A = 0 ℎ

Proof

Step Hyp Ref Expression
1 normcl.1 ⊢ A ∈ ℋ
2 norm-i ⊢ A ∈ ℋ → norm ℎ ⁡ A = 0 ↔ A = 0 ℎ
3 1 2 ax-mp ⊢ norm ℎ ⁡ A = 0 ↔ A = 0 ℎ