Theorem domnrcanb

Description: Right-cancellation law for domains, biconditional version of domnrcan . (Contributed by SN, 21-Jun-2025)

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

Proof

Step	Hyp	Ref	Expression
1		domnrcan.b	$$⊢B={\mathrm{Base}}_R$$
2		domnrcan.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		domnrcan.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		domnrcan.x	$$⊢\phi \to X\in B$$
5		domnrcan.y	$$⊢\phi \to Y\in B$$
6		domnrcan.z	$$⊢\phi \to Z\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
7		domnrcan.r	$$⊢\phi \to R\in \mathrm{Domn}$$
8		oveq1	$$⊢a=X\to a\underset{\dot{}}{·}c=X\underset{\dot{}}{·}c$$
9	8	eqeq1d	$$⊢a=X\to \left(a\underset{\dot{}}{·}c=b\underset{\dot{}}{·}c\leftrightarrow X\underset{\dot{}}{·}c=b\underset{\dot{}}{·}c\right)$$
10		eqeq1	$$⊢a=X\to \left(a=b\leftrightarrow X=b\right)$$
11	9 10	imbi12d	$$⊢a=X\to \left(\left(a\underset{\dot{}}{·}c=b\underset{\dot{}}{·}c\to a=b\right)\leftrightarrow \left(X\underset{\dot{}}{·}c=b\underset{\dot{}}{·}c\to X=b\right)\right)$$
12		oveq1	$$⊢b=Y\to b\underset{\dot{}}{·}c=Y\underset{\dot{}}{·}c$$
13	12	eqeq2d	$$⊢b=Y\to \left(X\underset{\dot{}}{·}c=b\underset{\dot{}}{·}c\leftrightarrow X\underset{\dot{}}{·}c=Y\underset{\dot{}}{·}c\right)$$
14		eqeq2	$$⊢b=Y\to \left(X=b\leftrightarrow X=Y\right)$$
15	13 14	imbi12d	$$⊢b=Y\to \left(\left(X\underset{\dot{}}{·}c=b\underset{\dot{}}{·}c\to X=b\right)\leftrightarrow \left(X\underset{\dot{}}{·}c=Y\underset{\dot{}}{·}c\to X=Y\right)\right)$$
16		oveq2	$$⊢c=Z\to X\underset{\dot{}}{·}c=X\underset{\dot{}}{·}Z$$
17		oveq2	$$⊢c=Z\to Y\underset{\dot{}}{·}c=Y\underset{\dot{}}{·}Z$$
18	16 17	eqeq12d	$$⊢c=Z\to \left(X\underset{\dot{}}{·}c=Y\underset{\dot{}}{·}c\leftrightarrow X\underset{\dot{}}{·}Z=Y\underset{\dot{}}{·}Z\right)$$
19	18	imbi1d	$$⊢c=Z\to \left(\left(X\underset{\dot{}}{·}c=Y\underset{\dot{}}{·}c\to X=Y\right)\leftrightarrow \left(X\underset{\dot{}}{·}Z=Y\underset{\dot{}}{·}Z\to X=Y\right)\right)$$
20	1 2 3	isdomn4r	$$⊢R\in \mathrm{Domn}\leftrightarrow \left(R\in \mathrm{NzRing}\wedge \forall a\in B\forall b\in B\forall c\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\left(a\underset{\dot{}}{·}c=b\underset{\dot{}}{·}c\to a=b\right)\right)$$
21	7 20	sylib	$$⊢\phi \to \left(R\in \mathrm{NzRing}\wedge \forall a\in B\forall b\in B\forall c\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\left(a\underset{\dot{}}{·}c=b\underset{\dot{}}{·}c\to a=b\right)\right)$$
22	21	simprd	$$⊢\phi \to \forall a\in B\forall b\in B\forall c\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\left(a\underset{\dot{}}{·}c=b\underset{\dot{}}{·}c\to a=b\right)$$
23	11 15 19 22 4 5 6	rspc3dv	$$⊢\phi \to \left(X\underset{\dot{}}{·}Z=Y\underset{\dot{}}{·}Z\to X=Y\right)$$
24		oveq1	$$⊢X=Y\to X\underset{\dot{}}{·}Z=Y\underset{\dot{}}{·}Z$$
25	23 24	impbid1	$$⊢\phi \to \left(X\underset{\dot{}}{·}Z=Y\underset{\dot{}}{·}Z\leftrightarrow X=Y\right)$$