Theorem isdomn2

Description: A ring is a domain iff all nonzero elements are regular elements. (Contributed by Mario Carneiro, 28-Mar-2015) (Proof shortened by SN, 21-Jun-2025)

	Ref	Expression
Hypotheses	isdomn2.b	|- B = ( Base ` R )
	isdomn2.t	|- E = ( RLReg ` R )
	isdomn2.z	|- .0. = ( 0g ` R )
Assertion	isdomn2	|- ( R e. Domn <-> ( R e. NzRing /\ ( B \ { .0. } ) C_ E ) )

Proof

Step	Hyp	Ref	Expression
1		isdomn2.b	|- B = ( Base ` R )
2		isdomn2.t	|- E = ( RLReg ` R )
3		isdomn2.z	|- .0. = ( 0g ` R )
4		eqid	|- ( .r ` R ) = ( .r ` R )
5	1 4 3	isdomn	|- ( R e. Domn <-> ( R e. NzRing /\ A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) )
6		eldifi	|- ( x e. ( B \ { .0. } ) -> x e. B )
7	2 1 4 3	isrrg	|- ( x e. E <-> ( x e. B /\ A. y e. B ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) ) )
8	7	baib	|- ( x e. B -> ( x e. E <-> A. y e. B ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) ) )
9	6 8	syl	|- ( x e. ( B \ { .0. } ) -> ( x e. E <-> A. y e. B ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) ) )
10	9	ralbiia	|- ( A. x e. ( B \ { .0. } ) x e. E <-> A. x e. ( B \ { .0. } ) A. y e. B ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) )
11		dfss3	|- ( ( B \ { .0. } ) C_ E <-> A. x e. ( B \ { .0. } ) x e. E )
12		isdomn5	|- ( A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) <-> A. x e. ( B \ { .0. } ) A. y e. B ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) )
13	10 11 12	3bitr4ri	|- ( A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) <-> ( B \ { .0. } ) C_ E )
14	13	anbi2i	|- ( ( R e. NzRing /\ A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) <-> ( R e. NzRing /\ ( B \ { .0. } ) C_ E ) )
15	5 14	bitri	|- ( R e. Domn <-> ( R e. NzRing /\ ( B \ { .0. } ) C_ E ) )