Theorem domnlcanbOLD

Description: Obsolete version of domnlcanb as of 21-Jun-2025. (Contributed by Thierry Arnoux, 8-Jun-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$$
	domnlcanbOLD.r	$$⊢\phi \to R\in \mathrm{Domn}$$
Assertion	domnlcanbOLD	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\leftrightarrow Y=Z\right)$$

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		domnlcanbOLD.r	$$⊢\phi \to R\in \mathrm{Domn}$$
8	4	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\right)\to X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
9	5	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\right)\to Y\in B$$
10	6	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\right)\to Z\in B$$
11	7	adantr	$$⊢\left(\phi \wedge X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\right)\to R\in \mathrm{Domn}$$
12		simpr	$$⊢\left(\phi \wedge X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\right)\to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z$$
13	1 2 3 8 9 10 11 12	domnlcan	$$⊢\left(\phi \wedge X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\right)\to Y=Z$$
14		simpr	$$⊢\left(\phi \wedge Y=Z\right)\to Y=Z$$
15	14	oveq2d	$$⊢\left(\phi \wedge Y=Z\right)\to X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z$$
16	13 15	impbida	$$⊢\phi \to \left(X\underset{\dot{}}{·}Y=X\underset{\dot{}}{·}Z\leftrightarrow Y=Z\right)$$