Metamath Proof Explorer

Theorem isdomn4

Description: A ring is a domain iff it is nonzero and the left cancellation law for multiplication holds. (Contributed by SN, 15-Sep-2024)

Ref Expression
Hypotheses isdomn4.b 
|- B = ( Base ` R )
isdomn4.0 
|- .0. = ( 0g ` R )
isdomn4.x 
|- .x. = ( .r ` R )
Assertion isdomn4 
|- ( R e. Domn <-> ( R e. NzRing /\ A. a e. ( B \ { .0. } ) A. b e. B A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) ) )

Proof

Step Hyp Ref Expression
1 isdomn4.b 
 |-  B = ( Base ` R )
2 isdomn4.0 
 |-  .0. = ( 0g ` R )
3 isdomn4.x 
 |-  .x. = ( .r ` R )
4 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
5 eqid 
 |-  ( -g ` R ) = ( -g ` R )
6 domnring 
 |-  ( R e. Domn -> R e. Ring )
7 6 adantr 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> R e. Ring )
8 eldifi 
 |-  ( a e. ( B \ { .0. } ) -> a e. B )
9 8 3ad2ant1 
 |-  ( ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) -> a e. B )
10 9 adantl 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> a e. B )
11 simpr2 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> b e. B )
12 simpr3 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> c e. B )
13 1 3 5 7 10 11 12 ringsubdi 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> ( a .x. ( b ( -g ` R ) c ) ) = ( ( a .x. b ) ( -g ` R ) ( a .x. c ) ) )
14 13 eqeq1d 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> ( ( a .x. ( b ( -g ` R ) c ) ) = .0. <-> ( ( a .x. b ) ( -g ` R ) ( a .x. c ) ) = .0. ) )
15 simpll 
 |-  ( ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) /\ ( b ( -g ` R ) c ) =/= .0. ) -> R e. Domn )
16 10 adantr 
 |-  ( ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) /\ ( b ( -g ` R ) c ) =/= .0. ) -> a e. B )
17 eldifsni 
 |-  ( a e. ( B \ { .0. } ) -> a =/= .0. )
18 17 3ad2ant1 
 |-  ( ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) -> a =/= .0. )
19 18 ad2antlr 
 |-  ( ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) /\ ( b ( -g ` R ) c ) =/= .0. ) -> a =/= .0. )
20 6 ringgrpd 
 |-  ( R e. Domn -> R e. Grp )
21 1 5 grpsubcl 
 |-  ( ( R e. Grp /\ b e. B /\ c e. B ) -> ( b ( -g ` R ) c ) e. B )
22 20 21 syl3an1 
 |-  ( ( R e. Domn /\ b e. B /\ c e. B ) -> ( b ( -g ` R ) c ) e. B )
23 22 3adant3r1 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> ( b ( -g ` R ) c ) e. B )
24 23 adantr 
 |-  ( ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) /\ ( b ( -g ` R ) c ) =/= .0. ) -> ( b ( -g ` R ) c ) e. B )
25 simpr 
 |-  ( ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) /\ ( b ( -g ` R ) c ) =/= .0. ) -> ( b ( -g ` R ) c ) =/= .0. )
26 1 3 2 domnmuln0 
 |-  ( ( R e. Domn /\ ( a e. B /\ a =/= .0. ) /\ ( ( b ( -g ` R ) c ) e. B /\ ( b ( -g ` R ) c ) =/= .0. ) ) -> ( a .x. ( b ( -g ` R ) c ) ) =/= .0. )
27 15 16 19 24 25 26 syl122anc 
 |-  ( ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) /\ ( b ( -g ` R ) c ) =/= .0. ) -> ( a .x. ( b ( -g ` R ) c ) ) =/= .0. )
28 27 ex 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> ( ( b ( -g ` R ) c ) =/= .0. -> ( a .x. ( b ( -g ` R ) c ) ) =/= .0. ) )
29 28 necon4d 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> ( ( a .x. ( b ( -g ` R ) c ) ) = .0. -> ( b ( -g ` R ) c ) = .0. ) )
30 14 29 sylbird 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> ( ( ( a .x. b ) ( -g ` R ) ( a .x. c ) ) = .0. -> ( b ( -g ` R ) c ) = .0. ) )
31 20 adantr 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> R e. Grp )
32 id 
 |-  ( b e. B -> b e. B )
33 1 3 ringcl 
 |-  ( ( R e. Ring /\ a e. B /\ b e. B ) -> ( a .x. b ) e. B )
34 6 8 32 33 syl3an 
 |-  ( ( R e. Domn /\ a e. ( B \ { .0. } ) /\ b e. B ) -> ( a .x. b ) e. B )
35 34 3adant3r3 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> ( a .x. b ) e. B )
36 id 
 |-  ( c e. B -> c e. B )
37 1 3 ringcl 
 |-  ( ( R e. Ring /\ a e. B /\ c e. B ) -> ( a .x. c ) e. B )
38 6 8 36 37 syl3an 
 |-  ( ( R e. Domn /\ a e. ( B \ { .0. } ) /\ c e. B ) -> ( a .x. c ) e. B )
39 38 3adant3r2 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> ( a .x. c ) e. B )
40 1 2 5 grpsubeq0 
 |-  ( ( R e. Grp /\ ( a .x. b ) e. B /\ ( a .x. c ) e. B ) -> ( ( ( a .x. b ) ( -g ` R ) ( a .x. c ) ) = .0. <-> ( a .x. b ) = ( a .x. c ) ) )
41 31 35 39 40 syl3anc 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> ( ( ( a .x. b ) ( -g ` R ) ( a .x. c ) ) = .0. <-> ( a .x. b ) = ( a .x. c ) ) )
42 1 2 5 grpsubeq0 
 |-  ( ( R e. Grp /\ b e. B /\ c e. B ) -> ( ( b ( -g ` R ) c ) = .0. <-> b = c ) )
43 31 11 12 42 syl3anc 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> ( ( b ( -g ` R ) c ) = .0. <-> b = c ) )
44 30 41 43 3imtr3d 
 |-  ( ( R e. Domn /\ ( a e. ( B \ { .0. } ) /\ b e. B /\ c e. B ) ) -> ( ( a .x. b ) = ( a .x. c ) -> b = c ) )
45 44 ralrimivvva 
 |-  ( R e. Domn -> A. a e. ( B \ { .0. } ) A. b e. B A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) )
46 4 45 jca 
 |-  ( R e. Domn -> ( R e. NzRing /\ A. a e. ( B \ { .0. } ) A. b e. B A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) ) )
47 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
48 47 ringgrpd 
 |-  ( R e. NzRing -> R e. Grp )
49 1 2 grpidcl 
 |-  ( R e. Grp -> .0. e. B )
50 48 49 syl 
 |-  ( R e. NzRing -> .0. e. B )
51 50 adantr 
 |-  ( ( R e. NzRing /\ ( a e. ( B \ { .0. } ) /\ b e. B ) ) -> .0. e. B )
52 oveq2 
 |-  ( c = .0. -> ( a .x. c ) = ( a .x. .0. ) )
53 52 eqeq2d 
 |-  ( c = .0. -> ( ( a .x. b ) = ( a .x. c ) <-> ( a .x. b ) = ( a .x. .0. ) ) )
54 eqeq2 
 |-  ( c = .0. -> ( b = c <-> b = .0. ) )
55 53 54 imbi12d 
 |-  ( c = .0. -> ( ( ( a .x. b ) = ( a .x. c ) -> b = c ) <-> ( ( a .x. b ) = ( a .x. .0. ) -> b = .0. ) ) )
56 55 rspcv 
 |-  ( .0. e. B -> ( A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) -> ( ( a .x. b ) = ( a .x. .0. ) -> b = .0. ) ) )
57 51 56 syl 
 |-  ( ( R e. NzRing /\ ( a e. ( B \ { .0. } ) /\ b e. B ) ) -> ( A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) -> ( ( a .x. b ) = ( a .x. .0. ) -> b = .0. ) ) )
58 1 3 2 ringrz 
 |-  ( ( R e. Ring /\ a e. B ) -> ( a .x. .0. ) = .0. )
59 47 8 58 syl2an 
 |-  ( ( R e. NzRing /\ a e. ( B \ { .0. } ) ) -> ( a .x. .0. ) = .0. )
60 59 adantrr 
 |-  ( ( R e. NzRing /\ ( a e. ( B \ { .0. } ) /\ b e. B ) ) -> ( a .x. .0. ) = .0. )
61 60 eqeq2d 
 |-  ( ( R e. NzRing /\ ( a e. ( B \ { .0. } ) /\ b e. B ) ) -> ( ( a .x. b ) = ( a .x. .0. ) <-> ( a .x. b ) = .0. ) )
62 61 imbi1d 
 |-  ( ( R e. NzRing /\ ( a e. ( B \ { .0. } ) /\ b e. B ) ) -> ( ( ( a .x. b ) = ( a .x. .0. ) -> b = .0. ) <-> ( ( a .x. b ) = .0. -> b = .0. ) ) )
63 57 62 sylibd 
 |-  ( ( R e. NzRing /\ ( a e. ( B \ { .0. } ) /\ b e. B ) ) -> ( A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) -> ( ( a .x. b ) = .0. -> b = .0. ) ) )
64 63 ralimdvva 
 |-  ( R e. NzRing -> ( A. a e. ( B \ { .0. } ) A. b e. B A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) -> A. a e. ( B \ { .0. } ) A. b e. B ( ( a .x. b ) = .0. -> b = .0. ) ) )
65 isdomn5 
 |-  ( A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) <-> A. a e. ( B \ { .0. } ) A. b e. B ( ( a .x. b ) = .0. -> b = .0. ) )
66 64 65 imbitrrdi 
 |-  ( R e. NzRing -> ( A. a e. ( B \ { .0. } ) A. b e. B A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) -> A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) )
67 66 imdistani 
 |-  ( ( R e. NzRing /\ A. a e. ( B \ { .0. } ) A. b e. B A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) ) -> ( R e. NzRing /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) )
68 1 3 2 isdomn 
 |-  ( R e. Domn <-> ( R e. NzRing /\ A. a e. B A. b e. B ( ( a .x. b ) = .0. -> ( a = .0. \/ b = .0. ) ) ) )
69 67 68 sylibr 
 |-  ( ( R e. NzRing /\ A. a e. ( B \ { .0. } ) A. b e. B A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) ) -> R e. Domn )
70 46 69 impbii 
 |-  ( R e. Domn <-> ( R e. NzRing /\ A. a e. ( B \ { .0. } ) A. b e. B A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) ) )