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

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 ) ) )