domnlcan

Description: Left-cancellation law for domains. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	domncan.b	\|- B = ( Base ` R )
	domncan.1	\|- .0. = ( 0g ` R )
	domncan.m	\|- .x. = ( .r ` R )
	domncan.x	\|- ( ph -> X e. ( B \ { .0. } ) )
	domncan.y	\|- ( ph -> Y e. B )
	domncan.z	\|- ( ph -> Z e. B )
	domnlcan.r	\|- ( ph -> R e. Domn )
	domnlcan.2	\|- ( ph -> ( X .x. Y ) = ( X .x. Z ) )
Assertion	domnlcan	\|- ( ph -> Y = Z )

Proof

Step	Hyp	Ref	Expression
1		domncan.b	\|- B = ( Base ` R )
2		domncan.1	\|- .0. = ( 0g ` R )
3		domncan.m	\|- .x. = ( .r ` R )
4		domncan.x	\|- ( ph -> X e. ( B \ { .0. } ) )
5		domncan.y	\|- ( ph -> Y e. B )
6		domncan.z	\|- ( ph -> Z e. B )
7		domnlcan.r	\|- ( ph -> R e. Domn )
8		domnlcan.2	\|- ( ph -> ( X .x. Y ) = ( X .x. Z ) )
9		oveq1	\|- ( a = X -> ( a .x. b ) = ( X .x. b ) )
10		oveq1	\|- ( a = X -> ( a .x. c ) = ( X .x. c ) )
11	9 10	eqeq12d	\|- ( a = X -> ( ( a .x. b ) = ( a .x. c ) <-> ( X .x. b ) = ( X .x. c ) ) )
12	11	imbi1d	\|- ( a = X -> ( ( ( a .x. b ) = ( a .x. c ) -> b = c ) <-> ( ( X .x. b ) = ( X .x. c ) -> b = c ) ) )
13		oveq2	\|- ( b = Y -> ( X .x. b ) = ( X .x. Y ) )
14	13	eqeq1d	\|- ( b = Y -> ( ( X .x. b ) = ( X .x. c ) <-> ( X .x. Y ) = ( X .x. c ) ) )
15		eqeq1	\|- ( b = Y -> ( b = c <-> Y = c ) )
16	14 15	imbi12d	\|- ( b = Y -> ( ( ( X .x. b ) = ( X .x. c ) -> b = c ) <-> ( ( X .x. Y ) = ( X .x. c ) -> Y = c ) ) )
17		oveq2	\|- ( c = Z -> ( X .x. c ) = ( X .x. Z ) )
18	17	eqeq2d	\|- ( c = Z -> ( ( X .x. Y ) = ( X .x. c ) <-> ( X .x. Y ) = ( X .x. Z ) ) )
19		eqeq2	\|- ( c = Z -> ( Y = c <-> Y = Z ) )
20	18 19	imbi12d	\|- ( c = Z -> ( ( ( X .x. Y ) = ( X .x. c ) -> Y = c ) <-> ( ( X .x. Y ) = ( X .x. Z ) -> Y = Z ) ) )
21	1 2 3	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 ) ) )
22	7 21	sylib	\|- ( ph -> ( R e. NzRing /\ A. a e. ( B \ { .0. } ) A. b e. B A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) ) )
23	22	simprd	\|- ( ph -> A. a e. ( B \ { .0. } ) A. b e. B A. c e. B ( ( a .x. b ) = ( a .x. c ) -> b = c ) )
24	12 16 20 23 4 5 6	rspc3dv	\|- ( ph -> ( ( X .x. Y ) = ( X .x. Z ) -> Y = Z ) )
25	8 24	mpd	\|- ( ph -> Y = Z )

Metamath Proof Explorer

Theorem domnlcan

Proof