Metamath Proof Explorer


Theorem nrgdomn

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

Ref Expression
Assertion nrgdomn ( 𝑅 ∈ NrmRing → ( 𝑅 ∈ Domn ↔ 𝑅 ∈ NzRing ) )

Proof

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