Theorem idomrcan

Description: Right-cancellation law for integral domains. (Contributed by Thierry Arnoux, 22-Mar-2025) (Proof shortened by SN, 21-Jun-2025)

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

Proof

Step	Hyp	Ref	Expression
1		idomrcan.b	|- B = ( Base ` R )
2		idomrcan.0	|- .0. = ( 0g ` R )
3		idomrcan.m	|- .x. = ( .r ` R )
4		idomrcan.x	|- ( ph -> X e. B )
5		idomrcan.y	|- ( ph -> Y e. B )
6		idomrcan.z	|- ( ph -> Z e. ( B \ { .0. } ) )
7		idomrcan.r	|- ( ph -> R e. IDomn )
8		idomrcan.1	|- ( ph -> ( X .x. Z ) = ( Y .x. Z ) )
9	7	idomdomd	|- ( ph -> R e. Domn )
10	1 2 3 4 5 6 9 8	domnrcan	|- ( ph -> X = Y )