Theorem domnlcanb

Description: Left-cancellation law for domains, biconditional version of domnlcan . (Contributed by Thierry Arnoux, 8-Jun-2025) Shorten this theorem and domnlcan overall. (Revised 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}$$
Assertion	domnlcanb	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\leftrightarrow Y=Z\right)$$

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		oveq1	$$⊢a=X\to a\underset{\dot{}}{·}b=X\underset{\dot{}}{·}b$$
9		oveq1	$$⊢a=X\to a\underset{\dot{}}{·}c=X\underset{\dot{}}{·}c$$
10	8 9	eqeq12d	$$⊢a=X\to \left(a\underset{\dot{}}{·}b=a\underset{\dot{}}{·}c\leftrightarrow X\underset{\dot{}}{·}b=X\underset{\dot{}}{·}c\right)$$
11	10	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)$$
12		oveq2	$$⊢b=Y\to X\underset{\dot{}}{·}b=X\underset{\dot{}}{·}Y$$
13	12	eqeq1d	$$⊢b=Y\to \left(X\underset{\dot{}}{·}b=X\underset{\dot{}}{·}c\leftrightarrow X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}c\right)$$
14		eqeq1	$$⊢b=Y\to \left(b=c\leftrightarrow Y=c\right)$$
15	13 14	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)$$
16		oveq2	$$⊢c=Z\to X\underset{\dot{}}{·}c=X\underset{\dot{}}{·}Z$$
17	16	eqeq2d	$$⊢c=Z\to \left(X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}c\leftrightarrow X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\right)$$
18		eqeq2	$$⊢c=Z\to \left(Y=c\leftrightarrow Y=Z\right)$$
19	17 18	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)$$
20	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)$$
21	7 20	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)$$
22	21	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)$$
23	11 15 19 22 4 5 6	rspc3dv	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\to Y=Z\right)$$
24		oveq2	$$⊢Y=Z\to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z$$
25	23 24	impbid1	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\leftrightarrow Y=Z\right)$$