Metamath Proof Explorer

Theorem isdomn2

Description: A ring is a domain iff all nonzero elements are nonzero-divisors. (Contributed by Mario Carneiro, 28-Mar-2015)

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 dfss3 
 |-  ( ( B \ { .0. } ) C_ E <-> A. x e. ( B \ { .0. } ) x e. E )
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 8 imbi2d 
 |-  ( x e. B -> ( ( x =/= .0. -> x e. E ) <-> ( x =/= .0. -> A. y e. B ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) ) ) )
10 9 ralbiia 
 |-  ( A. x e. B ( x =/= .0. -> x e. E ) <-> A. x e. B ( x =/= .0. -> A. y e. B ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) ) )
11 eldifsn 
 |-  ( x e. ( B \ { .0. } ) <-> ( x e. B /\ x =/= .0. ) )
12 11 imbi1i 
 |-  ( ( x e. ( B \ { .0. } ) -> x e. E ) <-> ( ( x e. B /\ x =/= .0. ) -> x e. E ) )
13 impexp 
 |-  ( ( ( x e. B /\ x =/= .0. ) -> x e. E ) <-> ( x e. B -> ( x =/= .0. -> x e. E ) ) )
14 12 13 bitri 
 |-  ( ( x e. ( B \ { .0. } ) -> x e. E ) <-> ( x e. B -> ( x =/= .0. -> x e. E ) ) )
15 14 ralbii2 
 |-  ( A. x e. ( B \ { .0. } ) x e. E <-> A. x e. B ( x =/= .0. -> x e. E ) )
16 con34b 
 |-  ( ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) <-> ( -. ( x = .0. \/ y = .0. ) -> -. ( x ( .r ` R ) y ) = .0. ) )
17 impexp 
 |-  ( ( ( -. x = .0. /\ -. y = .0. ) -> -. ( x ( .r ` R ) y ) = .0. ) <-> ( -. x = .0. -> ( -. y = .0. -> -. ( x ( .r ` R ) y ) = .0. ) ) )
18 ioran 
 |-  ( -. ( x = .0. \/ y = .0. ) <-> ( -. x = .0. /\ -. y = .0. ) )
19 18 imbi1i 
 |-  ( ( -. ( x = .0. \/ y = .0. ) -> -. ( x ( .r ` R ) y ) = .0. ) <-> ( ( -. x = .0. /\ -. y = .0. ) -> -. ( x ( .r ` R ) y ) = .0. ) )
20 df-ne 
 |-  ( x =/= .0. <-> -. x = .0. )
21 con34b 
 |-  ( ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) <-> ( -. y = .0. -> -. ( x ( .r ` R ) y ) = .0. ) )
22 20 21 imbi12i 
 |-  ( ( x =/= .0. -> ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) ) <-> ( -. x = .0. -> ( -. y = .0. -> -. ( x ( .r ` R ) y ) = .0. ) ) )
23 17 19 22 3bitr4i 
 |-  ( ( -. ( x = .0. \/ y = .0. ) -> -. ( x ( .r ` R ) y ) = .0. ) <-> ( x =/= .0. -> ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) ) )
24 16 23 bitri 
 |-  ( ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) <-> ( x =/= .0. -> ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) ) )
25 24 ralbii 
 |-  ( A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) <-> A. y e. B ( x =/= .0. -> ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) ) )
26 r19.21v 
 |-  ( A. y e. B ( x =/= .0. -> ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) ) <-> ( x =/= .0. -> A. y e. B ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) ) )
27 25 26 bitri 
 |-  ( A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) <-> ( x =/= .0. -> A. y e. B ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) ) )
28 27 ralbii 
 |-  ( A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) <-> A. x e. B ( x =/= .0. -> A. y e. B ( ( x ( .r ` R ) y ) = .0. -> y = .0. ) ) )
29 10 15 28 3bitr4i 
 |-  ( A. x e. ( B \ { .0. } ) x e. E <-> A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) )
30 6 29 bitr2i 
 |-  ( A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) <-> ( B \ { .0. } ) C_ E )
31 30 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 ) )
32 5 31 bitri 
 |-  ( R e. Domn <-> ( R e. NzRing /\ ( B \ { .0. } ) C_ E ) )