Metamath Proof Explorer

Theorem nrgdomn

Description: A nonzero normed ring is a domain. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion nrgdomn ⊢ R ∈ NrmRing → R ∈ Domn ↔ R ∈ NzRing

Proof

Step Hyp Ref Expression
1 domnnzr ⊢ R ∈ Domn → R ∈ NzRing
2 simpr ⊢ R ∈ NrmRing ∧ R ∈ NzRing → R ∈ NzRing
3 eqid ⊢ norm ⁡ R = norm ⁡ R
4 eqid ⊢ AbsVal ⁡ R = AbsVal ⁡ R
5 3 4 nrgabv ⊢ R ∈ NrmRing → norm ⁡ R ∈ AbsVal ⁡ R
6 5 ne0d ⊢ R ∈ NrmRing → AbsVal ⁡ R ≠ ∅
7 6 adantr ⊢ R ∈ NrmRing ∧ R ∈ NzRing → AbsVal ⁡ R ≠ ∅
8 4 abvn0b ⊢ R ∈ Domn ↔ R ∈ NzRing ∧ AbsVal ⁡ R ≠ ∅
9 2 7 8 sylanbrc ⊢ R ∈ NrmRing ∧ R ∈ NzRing → R ∈ Domn
10 9 ex ⊢ R ∈ NrmRing → R ∈ NzRing → R ∈ Domn
11 1 10 impbid2 ⊢ R ∈ NrmRing → R ∈ Domn ↔ R ∈ NzRing