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

Metamath Proof Explorer

Theorem isdomn6

Description: A ring is a domain iff the regular elements are the nonzero elements. Compare isdomn2 , domnrrg . (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 ) )