Theorem isdomn6

Description: A ring is a domain iff nonzero-divisors are all the nonzero elements. (Contributed by Thierry Arnoux, 6-May-2025)

	Ref	Expression
Hypotheses	isdomn6.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isdomn6.t	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
	isdomn6.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	isdomn6	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ( 𝐵 ∖ { 0 } ) = 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		isdomn6.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isdomn6.t	⊢ 𝐸 = ( RLReg ‘ 𝑅 )
3		isdomn6.z	⊢ 0 = ( 0g ‘ 𝑅 )
4	1 2 3	isdomn2	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ( 𝐵 ∖ { 0 } ) ⊆ 𝐸 ) )
5	2 1	rrgss	⊢ 𝐸 ⊆ 𝐵
6	5	a1i	⊢ ( 𝑅 ∈ NzRing → 𝐸 ⊆ 𝐵 )
7	2 3	rrgnz	⊢ ( 𝑅 ∈ NzRing → ¬ 0 ∈ 𝐸 )
8		ssdifsn	⊢ ( 𝐸 ⊆ ( 𝐵 ∖ { 0 } ) ↔ ( 𝐸 ⊆ 𝐵 ∧ ¬ 0 ∈ 𝐸 ) )
9	6 7 8	sylanbrc	⊢ ( 𝑅 ∈ NzRing → 𝐸 ⊆ ( 𝐵 ∖ { 0 } ) )
10		sssseq	⊢ ( 𝐸 ⊆ ( 𝐵 ∖ { 0 } ) → ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐸 ↔ ( 𝐵 ∖ { 0 } ) = 𝐸 ) )
11	9 10	syl	⊢ ( 𝑅 ∈ NzRing → ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐸 ↔ ( 𝐵 ∖ { 0 } ) = 𝐸 ) )
12	11	pm5.32i	⊢ ( ( 𝑅 ∈ NzRing ∧ ( 𝐵 ∖ { 0 } ) ⊆ 𝐸 ) ↔ ( 𝑅 ∈ NzRing ∧ ( 𝐵 ∖ { 0 } ) = 𝐸 ) )
13	4 12	bitri	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ( 𝐵 ∖ { 0 } ) = 𝐸 ) )