Theorem domnlcanOLD

Description: Obsolete version of domnlcan as of 21-Jun-2025. (Contributed by Thierry Arnoux, 22-Mar-2025) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		domncanOLD.b	$$⊢B={\mathrm{Base}}_R$$
2		domncanOLD.1	$$⊢\underset{\dot{}}{0}=0_R$$
3		domncanOLD.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		domncanOLD.x	$$⊢\phi \to X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
5		domncanOLD.y	$$⊢\phi \to Y\in B$$
6		domncanOLD.z	$$⊢\phi \to Z\in B$$
7		domnlcanOLD.r	$$⊢\phi \to R\in \mathrm{Domn}$$
8		domnlcanOLD.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$$