Theorem domnnzr

Description: A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015)

	Ref	Expression
Assertion	domnnzr	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
2		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
3		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
4	1 2 3	isdomn	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0g ‘ 𝑅 ) → ( 𝑥 = ( 0g ‘ 𝑅 ) ∨ 𝑦 = ( 0g ‘ 𝑅 ) ) ) ) )
5	4	simplbi	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )