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

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 ) )