Metamath Proof Explorer

Theorem isdomn4r

Description: A ring is a domain iff it is nonzero and the right cancellation law for multiplication holds. (Contributed by SN, 20-Jun-2025)

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

Proof

Step Hyp Ref Expression
1 isdomn4r.b 
 |-  B = ( Base ` R )
2 isdomn4r.0 
 |-  .0. = ( 0g ` R )
3 isdomn4r.x 
 |-  .x. = ( .r ` R )
4 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
5 4 1 opprbas 
 |-  B = ( Base ` ( oppR ` R ) )
6 4 2 oppr0 
 |-  .0. = ( 0g ` ( oppR ` R ) )
7 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
8 5 6 7 isdomn4 
 |-  ( ( oppR ` R ) e. Domn <-> ( ( oppR ` R ) e. NzRing /\ A. c e. ( B \ { .0. } ) A. a e. B A. b e. B ( ( c ( .r ` ( oppR ` R ) ) a ) = ( c ( .r ` ( oppR ` R ) ) b ) -> a = b ) ) )
9 4 opprdomnb 
 |-  ( R e. Domn <-> ( oppR ` R ) e. Domn )
10 4 opprnzrb 
 |-  ( R e. NzRing <-> ( oppR ` R ) e. NzRing )
11 1 3 4 7 opprmul 
 |-  ( c ( .r ` ( oppR ` R ) ) a ) = ( a .x. c )
12 1 3 4 7 opprmul 
 |-  ( c ( .r ` ( oppR ` R ) ) b ) = ( b .x. c )
13 11 12 eqeq12i 
 |-  ( ( c ( .r ` ( oppR ` R ) ) a ) = ( c ( .r ` ( oppR ` R ) ) b ) <-> ( a .x. c ) = ( b .x. c ) )
14 13 imbi1i 
 |-  ( ( ( c ( .r ` ( oppR ` R ) ) a ) = ( c ( .r ` ( oppR ` R ) ) b ) -> a = b ) <-> ( ( a .x. c ) = ( b .x. c ) -> a = b ) )
15 14 3ralbii 
 |-  ( A. a e. B A. b e. B A. c e. ( B \ { .0. } ) ( ( c ( .r ` ( oppR ` R ) ) a ) = ( c ( .r ` ( oppR ` R ) ) b ) -> a = b ) <-> A. a e. B A. b e. B A. c e. ( B \ { .0. } ) ( ( a .x. c ) = ( b .x. c ) -> a = b ) )
16 ralrot3 
 |-  ( A. a e. B A. b e. B A. c e. ( B \ { .0. } ) ( ( c ( .r ` ( oppR ` R ) ) a ) = ( c ( .r ` ( oppR ` R ) ) b ) -> a = b ) <-> A. c e. ( B \ { .0. } ) A. a e. B A. b e. B ( ( c ( .r ` ( oppR ` R ) ) a ) = ( c ( .r ` ( oppR ` R ) ) b ) -> a = b ) )
17 15 16 bitr3i 
 |-  ( A. a e. B A. b e. B A. c e. ( B \ { .0. } ) ( ( a .x. c ) = ( b .x. c ) -> a = b ) <-> A. c e. ( B \ { .0. } ) A. a e. B A. b e. B ( ( c ( .r ` ( oppR ` R ) ) a ) = ( c ( .r ` ( oppR ` R ) ) b ) -> a = b ) )
18 10 17 anbi12i 
 |-  ( ( R e. NzRing /\ A. a e. B A. b e. B A. c e. ( B \ { .0. } ) ( ( a .x. c ) = ( b .x. c ) -> a = b ) ) <-> ( ( oppR ` R ) e. NzRing /\ A. c e. ( B \ { .0. } ) A. a e. B A. b e. B ( ( c ( .r ` ( oppR ` R ) ) a ) = ( c ( .r ` ( oppR ` R ) ) b ) -> a = b ) ) )
19 8 9 18 3bitr4i 
 |-  ( R e. Domn <-> ( R e. NzRing /\ A. a e. B A. b e. B A. c e. ( B \ { .0. } ) ( ( a .x. c ) = ( b .x. c ) -> a = b ) ) )