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	|- B = ( Base ` R )
	isdomn6.t	|- E = ( RLReg ` R )
	isdomn6.z	|- .0. = ( 0g ` R )
Assertion	isdomn6	|- ( R e. Domn <-> ( R e. NzRing /\ ( B \ { .0. } ) = E ) )

Proof

Step	Hyp	Ref	Expression
1		isdomn6.b	|- B = ( Base ` R )
2		isdomn6.t	|- E = ( RLReg ` R )
3		isdomn6.z	|- .0. = ( 0g ` R )
4	1 2 3	isdomn2	|- ( R e. Domn <-> ( R e. NzRing /\ ( B \ { .0. } ) C_ E ) )
5	2 1	rrgss	|- E C_ B
6	5	a1i	|- ( R e. NzRing -> E C_ B )
7	2 3	rrgnz	|- ( R e. NzRing -> -. .0. e. E )
8		ssdifsn	|- ( E C_ ( B \ { .0. } ) <-> ( E C_ B /\ -. .0. e. E ) )
9	6 7 8	sylanbrc	|- ( R e. NzRing -> E C_ ( B \ { .0. } ) )
10		sssseq	|- ( E C_ ( B \ { .0. } ) -> ( ( B \ { .0. } ) C_ E <-> ( B \ { .0. } ) = E ) )
11	9 10	syl	|- ( R e. NzRing -> ( ( B \ { .0. } ) C_ E <-> ( B \ { .0. } ) = E ) )
12	11	pm5.32i	|- ( ( R e. NzRing /\ ( B \ { .0. } ) C_ E ) <-> ( R e. NzRing /\ ( B \ { .0. } ) = E ) )
13	4 12	bitri	|- ( R e. Domn <-> ( R e. NzRing /\ ( B \ { .0. } ) = E ) )