Theorem domnlcan

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

	Ref	Expression
Hypotheses	domncan.b	$$⊢B={\mathrm{Base}}_R$$
	domncan.0	$$⊢\underset{\dot{}}{0}=0_R$$
	domncan.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	domncan.x	$$⊢\phi \to X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	domncan.y	$$⊢\phi \to Y\in B$$
	domncan.z	$$⊢\phi \to Z\in B$$
	domncan.r	$$⊢\phi \to R\in \mathrm{Domn}$$
	domnlcan.1	$$⊢\phi \to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z$$
Assertion	domnlcan	$$⊢\phi \to Y=Z$$

Proof

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