Theorem domnlcan

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

	Ref	Expression
Hypotheses	domncan.b	$$⊢B={\mathrm{Base}}_R$$
	domncan.1	$$⊢\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$$
	domnlcan.r	$$⊢\phi \to R\in \mathrm{Domn}$$
	domnlcan.2	$$⊢\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.1	$$⊢\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		domnlcan.r	$$⊢\phi \to R\in \mathrm{Domn}$$
8		domnlcan.2	$$⊢\phi \to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z$$
9		oveq1	$$⊢a=X\to a\underset{\dot{}}{·}b=X\underset{\dot{}}{·}b$$
10		oveq1	$$⊢a=X\to a\underset{\dot{}}{·}c=X\underset{\dot{}}{·}c$$
11	9 10	eqeq12d	$$⊢a=X\to \left(a\underset{\dot{}}{·}b=a\underset{\dot{}}{·}c\leftrightarrow X\underset{\dot{}}{·}b=X\underset{\dot{}}{·}c\right)$$
12	11	imbi1d	$$⊢a=X\to \left(\left(a\underset{\dot{}}{·}b=a\underset{\dot{}}{·}c\to b=c\right)\leftrightarrow \left(X\underset{\dot{}}{·}b=X\underset{\dot{}}{·}c\to b=c\right)\right)$$
13		oveq2	$$⊢b=Y\to X\underset{\dot{}}{·}b=X\underset{\dot{}}{·}Y$$
14	13	eqeq1d	$$⊢b=Y\to \left(X\underset{\dot{}}{·}b=X\underset{\dot{}}{·}c\leftrightarrow X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}c\right)$$
15		eqeq1	$$⊢b=Y\to \left(b=c\leftrightarrow Y=c\right)$$
16	14 15	imbi12d	$$⊢b=Y\to \left(\left(X\underset{\dot{}}{·}b=X\underset{\dot{}}{·}c\to b=c\right)\leftrightarrow \left(X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}c\to Y=c\right)\right)$$
17		oveq2	$$⊢c=Z\to X\underset{\dot{}}{·}c=X\underset{\dot{}}{·}Z$$
18	17	eqeq2d	$$⊢c=Z\to \left(X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}c\leftrightarrow X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\right)$$
19		eqeq2	$$⊢c=Z\to \left(Y=c\leftrightarrow Y=Z\right)$$
20	18 19	imbi12d	$$⊢c=Z\to \left(\left(X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}c\to Y=c\right)\leftrightarrow \left(X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\to Y=Z\right)\right)$$
21	1 2 3	isdomn4	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge \forall a\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\forall b\in B\forall c\in B\left(a\underset{\dot{}}{·}b=a\underset{\dot{}}{·}c\to b=c\right)\right)$$
22	7 21	sylib	$$⊢\phi \to \left(R\in \mathrm{NzRing}\wedge \forall a\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\forall b\in B\forall c\in B\left(a\underset{\dot{}}{·}b=a\underset{\dot{}}{·}c\to b=c\right)\right)$$
23	22	simprd	$$⊢\phi \to \forall a\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\forall b\in B\forall c\in B\left(a\underset{\dot{}}{·}b=a\underset{\dot{}}{·}c\to b=c\right)$$
24	12 16 20 23 4 5 6	rspc3dv	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\to Y=Z\right)$$
25	8 24	mpd	$$⊢\phi \to Y=Z$$