Theorem idomrcan

Description: Right-cancellation law for integral 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 )
	domnrcan.r	|- ( ph -> R e. IDomn )
	domnrcan.2	|- ( ph -> ( Y .x. X ) = ( Z .x. X ) )
Assertion	idomrcan	|- ( 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		domnrcan.r	|- ( ph -> R e. IDomn )
8		domnrcan.2	|- ( ph -> ( Y .x. X ) = ( Z .x. X ) )
9	7	idomdomd	|- ( ph -> R e. Domn )
10		df-idom	|- IDomn = ( CRing i^i Domn )
11	7 10	eleqtrdi	|- ( ph -> R e. ( CRing i^i Domn ) )
12	11	elin1d	|- ( ph -> R e. CRing )
13	4	eldifad	|- ( ph -> X e. B )
14	1 3	crngcom	|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( X .x. Y ) = ( Y .x. X ) )
15	12 13 5 14	syl3anc	|- ( ph -> ( X .x. Y ) = ( Y .x. X ) )
16	1 3	crngcom	|- ( ( R e. CRing /\ X e. B /\ Z e. B ) -> ( X .x. Z ) = ( Z .x. X ) )
17	12 13 6 16	syl3anc	|- ( ph -> ( X .x. Z ) = ( Z .x. X ) )
18	8 15 17	3eqtr4d	|- ( ph -> ( X .x. Y ) = ( X .x. Z ) )
19	1 2 3 4 5 6 9 18	domnlcan	|- ( ph -> Y = Z )