This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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