Metamath Proof Explorer

Theorem isdomn3

Description: Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015)

Ref Expression
Hypotheses isdomn3.b 
|- B = ( Base ` R )
isdomn3.z 
|- .0. = ( 0g ` R )
isdomn3.u 
|- U = ( mulGrp ` R )
Assertion isdomn3 
|- ( R e. Domn <-> ( R e. Ring /\ ( B \ { .0. } ) e. ( SubMnd ` U ) ) )

Proof

Step Hyp Ref Expression
1 isdomn3.b 
 |-  B = ( Base ` R )
2 isdomn3.z 
 |-  .0. = ( 0g ` R )
3 isdomn3.u 
 |-  U = ( mulGrp ` R )
4 eqid 
 |-  ( .r ` R ) = ( .r ` R )
5 1 4 2 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 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
7 6 2 isnzr 
 |-  ( R e. NzRing <-> ( R e. Ring /\ ( 1r ` R ) =/= .0. ) )
8 7 anbi1i 
 |-  ( ( R e. NzRing /\ A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) <-> ( ( R e. Ring /\ ( 1r ` R ) =/= .0. ) /\ A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) )
9 anass 
 |-  ( ( ( R e. Ring /\ ( 1r ` R ) =/= .0. ) /\ A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) <-> ( R e. Ring /\ ( ( 1r ` R ) =/= .0. /\ A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) ) )
10 8 9 bitri 
 |-  ( ( R e. NzRing /\ A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) <-> ( R e. Ring /\ ( ( 1r ` R ) =/= .0. /\ A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) ) )
11 1 6 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
12 eldifsn 
 |-  ( ( 1r ` R ) e. ( B \ { .0. } ) <-> ( ( 1r ` R ) e. B /\ ( 1r ` R ) =/= .0. ) )
13 12 baibr 
 |-  ( ( 1r ` R ) e. B -> ( ( 1r ` R ) =/= .0. <-> ( 1r ` R ) e. ( B \ { .0. } ) ) )
14 11 13 syl 
 |-  ( R e. Ring -> ( ( 1r ` R ) =/= .0. <-> ( 1r ` R ) e. ( B \ { .0. } ) ) )
15 1 4 ringcl 
 |-  ( ( R e. Ring /\ x e. B /\ y e. B ) -> ( x ( .r ` R ) y ) e. B )
16 15 3expb 
 |-  ( ( R e. Ring /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` R ) y ) e. B )
17 16 biantrurd 
 |-  ( ( R e. Ring /\ ( x e. B /\ y e. B ) ) -> ( ( x ( .r ` R ) y ) =/= .0. <-> ( ( x ( .r ` R ) y ) e. B /\ ( x ( .r ` R ) y ) =/= .0. ) ) )
18 eldifsn 
 |-  ( ( x ( .r ` R ) y ) e. ( B \ { .0. } ) <-> ( ( x ( .r ` R ) y ) e. B /\ ( x ( .r ` R ) y ) =/= .0. ) )
19 17 18 bitr4di 
 |-  ( ( R e. Ring /\ ( x e. B /\ y e. B ) ) -> ( ( x ( .r ` R ) y ) =/= .0. <-> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) )
20 19 imbi2d 
 |-  ( ( R e. Ring /\ ( x e. B /\ y e. B ) ) -> ( ( ( x =/= .0. /\ y =/= .0. ) -> ( x ( .r ` R ) y ) =/= .0. ) <-> ( ( x =/= .0. /\ y =/= .0. ) -> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) ) )
21 20 2ralbidva 
 |-  ( R e. Ring -> ( A. x e. B A. y e. B ( ( x =/= .0. /\ y =/= .0. ) -> ( x ( .r ` R ) y ) =/= .0. ) <-> A. x e. B A. y e. B ( ( x =/= .0. /\ y =/= .0. ) -> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) ) )
22 con34b 
 |-  ( ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) <-> ( -. ( x = .0. \/ y = .0. ) -> -. ( x ( .r ` R ) y ) = .0. ) )
23 neanior 
 |-  ( ( x =/= .0. /\ y =/= .0. ) <-> -. ( x = .0. \/ y = .0. ) )
24 df-ne 
 |-  ( ( x ( .r ` R ) y ) =/= .0. <-> -. ( x ( .r ` R ) y ) = .0. )
25 23 24 imbi12i 
 |-  ( ( ( x =/= .0. /\ y =/= .0. ) -> ( x ( .r ` R ) y ) =/= .0. ) <-> ( -. ( x = .0. \/ y = .0. ) -> -. ( x ( .r ` R ) y ) = .0. ) )
26 22 25 bitr4i 
 |-  ( ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) <-> ( ( x =/= .0. /\ y =/= .0. ) -> ( x ( .r ` R ) y ) =/= .0. ) )
27 26 2ralbii 
 |-  ( A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) <-> A. x e. B A. y e. B ( ( x =/= .0. /\ y =/= .0. ) -> ( x ( .r ` R ) y ) =/= .0. ) )
28 impexp 
 |-  ( ( ( ( x e. B /\ y e. B ) /\ ( x =/= .0. /\ y =/= .0. ) ) -> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) <-> ( ( x e. B /\ y e. B ) -> ( ( x =/= .0. /\ y =/= .0. ) -> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) ) )
29 an4 
 |-  ( ( ( x e. B /\ y e. B ) /\ ( x =/= .0. /\ y =/= .0. ) ) <-> ( ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) )
30 eldifsn 
 |-  ( x e. ( B \ { .0. } ) <-> ( x e. B /\ x =/= .0. ) )
31 eldifsn 
 |-  ( y e. ( B \ { .0. } ) <-> ( y e. B /\ y =/= .0. ) )
32 30 31 anbi12i 
 |-  ( ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) <-> ( ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) )
33 29 32 bitr4i 
 |-  ( ( ( x e. B /\ y e. B ) /\ ( x =/= .0. /\ y =/= .0. ) ) <-> ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) )
34 33 imbi1i 
 |-  ( ( ( ( x e. B /\ y e. B ) /\ ( x =/= .0. /\ y =/= .0. ) ) -> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) <-> ( ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) -> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) )
35 28 34 bitr3i 
 |-  ( ( ( x e. B /\ y e. B ) -> ( ( x =/= .0. /\ y =/= .0. ) -> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) ) <-> ( ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) -> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) )
36 35 2albii 
 |-  ( A. x A. y ( ( x e. B /\ y e. B ) -> ( ( x =/= .0. /\ y =/= .0. ) -> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) ) <-> A. x A. y ( ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) -> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) )
37 r2al 
 |-  ( A. x e. B A. y e. B ( ( x =/= .0. /\ y =/= .0. ) -> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) <-> A. x A. y ( ( x e. B /\ y e. B ) -> ( ( x =/= .0. /\ y =/= .0. ) -> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) ) )
38 r2al 
 |-  ( A. x e. ( B \ { .0. } ) A. y e. ( B \ { .0. } ) ( x ( .r ` R ) y ) e. ( B \ { .0. } ) <-> A. x A. y ( ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) -> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) )
39 36 37 38 3bitr4ri 
 |-  ( A. x e. ( B \ { .0. } ) A. y e. ( B \ { .0. } ) ( x ( .r ` R ) y ) e. ( B \ { .0. } ) <-> A. x e. B A. y e. B ( ( x =/= .0. /\ y =/= .0. ) -> ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) )
40 21 27 39 3bitr4g 
 |-  ( R e. Ring -> ( 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 \ { .0. } ) ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) )
41 14 40 anbi12d 
 |-  ( R e. Ring -> ( ( ( 1r ` R ) =/= .0. /\ A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) <-> ( ( 1r ` R ) e. ( B \ { .0. } ) /\ A. x e. ( B \ { .0. } ) A. y e. ( B \ { .0. } ) ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) ) )
42 3 ringmgp 
 |-  ( R e. Ring -> U e. Mnd )
43 3 1 mgpbas 
 |-  B = ( Base ` U )
44 3 6 ringidval 
 |-  ( 1r ` R ) = ( 0g ` U )
45 3 4 mgpplusg 
 |-  ( .r ` R ) = ( +g ` U )
46 43 44 45 issubm 
 |-  ( U e. Mnd -> ( ( B \ { .0. } ) e. ( SubMnd ` U ) <-> ( ( B \ { .0. } ) C_ B /\ ( 1r ` R ) e. ( B \ { .0. } ) /\ A. x e. ( B \ { .0. } ) A. y e. ( B \ { .0. } ) ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) ) )
47 3anass 
 |-  ( ( ( B \ { .0. } ) C_ B /\ ( 1r ` R ) e. ( B \ { .0. } ) /\ A. x e. ( B \ { .0. } ) A. y e. ( B \ { .0. } ) ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) <-> ( ( B \ { .0. } ) C_ B /\ ( ( 1r ` R ) e. ( B \ { .0. } ) /\ A. x e. ( B \ { .0. } ) A. y e. ( B \ { .0. } ) ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) ) )
48 46 47 bitrdi 
 |-  ( U e. Mnd -> ( ( B \ { .0. } ) e. ( SubMnd ` U ) <-> ( ( B \ { .0. } ) C_ B /\ ( ( 1r ` R ) e. ( B \ { .0. } ) /\ A. x e. ( B \ { .0. } ) A. y e. ( B \ { .0. } ) ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) ) ) )
49 difss 
 |-  ( B \ { .0. } ) C_ B
50 49 biantrur 
 |-  ( ( ( 1r ` R ) e. ( B \ { .0. } ) /\ A. x e. ( B \ { .0. } ) A. y e. ( B \ { .0. } ) ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) <-> ( ( B \ { .0. } ) C_ B /\ ( ( 1r ` R ) e. ( B \ { .0. } ) /\ A. x e. ( B \ { .0. } ) A. y e. ( B \ { .0. } ) ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) ) )
51 48 50 bitr4di 
 |-  ( U e. Mnd -> ( ( B \ { .0. } ) e. ( SubMnd ` U ) <-> ( ( 1r ` R ) e. ( B \ { .0. } ) /\ A. x e. ( B \ { .0. } ) A. y e. ( B \ { .0. } ) ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) ) )
52 42 51 syl 
 |-  ( R e. Ring -> ( ( B \ { .0. } ) e. ( SubMnd ` U ) <-> ( ( 1r ` R ) e. ( B \ { .0. } ) /\ A. x e. ( B \ { .0. } ) A. y e. ( B \ { .0. } ) ( x ( .r ` R ) y ) e. ( B \ { .0. } ) ) ) )
53 41 52 bitr4d 
 |-  ( R e. Ring -> ( ( ( 1r ` R ) =/= .0. /\ A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) <-> ( B \ { .0. } ) e. ( SubMnd ` U ) ) )
54 53 pm5.32i 
 |-  ( ( R e. Ring /\ ( ( 1r ` R ) =/= .0. /\ A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) ) <-> ( R e. Ring /\ ( B \ { .0. } ) e. ( SubMnd ` U ) ) )
55 10 54 bitri 
 |-  ( ( R e. NzRing /\ A. x e. B A. y e. B ( ( x ( .r ` R ) y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) <-> ( R e. Ring /\ ( B \ { .0. } ) e. ( SubMnd ` U ) ) )
56 5 55 bitri 
 |-  ( R e. Domn <-> ( R e. Ring /\ ( B \ { .0. } ) e. ( SubMnd ` U ) ) )