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