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={\mathrm{Base}}_R$$
	idomrcan.0	$$⊢\underset{\dot{}}{0}=0_R$$
	idomrcan.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	idomrcan.x	$$⊢\phi \to X\in B$$
	idomrcan.y	$$⊢\phi \to Y\in B$$
	idomrcan.z	$$⊢\phi \to Z\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	idomrcan.r	$$⊢\phi \to R\in \mathrm{IDomn}$$
	idomrcan.1	$$⊢\phi \to X\underset{\dot{}}{·}Z=Y\underset{\dot{}}{·}Z$$
Assertion	idomrcan	$$⊢\phi \to X=Y$$

Proof

Step	Hyp	Ref	Expression
1		idomrcan.b	$$⊢B={\mathrm{Base}}_R$$
2		idomrcan.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		idomrcan.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		idomrcan.x	$$⊢\phi \to X\in B$$
5		idomrcan.y	$$⊢\phi \to Y\in B$$
6		idomrcan.z	$$⊢\phi \to Z\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
7		idomrcan.r	$$⊢\phi \to R\in \mathrm{IDomn}$$
8		idomrcan.1	$$⊢\phi \to X\underset{\dot{}}{·}Z=Y\underset{\dot{}}{·}Z$$
9	7	idomdomd	$$⊢\phi \to R\in \mathrm{Domn}$$
10	1 2 3 4 5 6 9 8	domnrcan	$$⊢\phi \to X=Y$$