Theorem idomrcanOLD

Description: Obsolete version of idomrcan 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$$
	idomrcanOLD.r	$$⊢\phi \to R\in \mathrm{IDomn}$$
	idomrcanOLD.2	$$⊢\phi \to Y\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}X$$
Assertion	idomrcanOLD	$$⊢\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		idomrcanOLD.r	$$⊢\phi \to R\in \mathrm{IDomn}$$
8		idomrcanOLD.2	$$⊢\phi \to Y\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}X$$
9	7	idomdomd	$$⊢\phi \to R\in \mathrm{Domn}$$
10		df-idom	$$⊢\mathrm{IDomn}=\mathrm{CRing}\cap \mathrm{Domn}$$
11	7 10	eleqtrdi	$$⊢\phi \to R\in \left(\mathrm{CRing}\cap \mathrm{Domn}\right)$$
12	11	elin1d	$$⊢\phi \to R\in \mathrm{CRing}$$
13	4	eldifad	$$⊢\phi \to X\in B$$
14	1 3	crngcom	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{·}Y=Y\underset{\dot{}}{·}X$$
15	12 13 5 14	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}Y=Y\underset{\dot{}}{·}X$$
16	1 3	crngcom	$$⊢\left(R\in \mathrm{CRing}\wedge X\in B\wedge Z\in B\right)\to X\underset{\dot{}}{·}Z=Z\underset{\dot{}}{·}X$$
17	12 13 6 16	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}Z=Z\underset{\dot{}}{·}X$$
18	8 15 17	3eqtr4d	$$⊢\phi \to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z$$
19	1 2 3 4 5 6 9 18	domnlcan	$$⊢\phi \to Y=Z$$