Theorem drngmullcan

Description: Cancellation of a nonzero factor on the left for multiplication. ( mulcanad analog). (Contributed by SN, 14-Aug-2024) (Proof shortened by SN, 25-Jun-2025)

	Ref	Expression
Hypotheses	drngmullcan.b	$$⊢B={\mathrm{Base}}_R$$
	drngmullcan.0	$$⊢\underset{\dot{}}{0}=0_R$$
	drngmullcan.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	drngmullcan.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
	drngmullcan.x	$$⊢\phi \to X\in B$$
	drngmullcan.y	$$⊢\phi \to Y\in B$$
	drngmullcan.z	$$⊢\phi \to Z\in B$$
	drngmullcan.1	$$⊢\phi \to Z\ne \underset{\dot{}}{0}$$
	drngmullcan.2	$$⊢\phi \to Z\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}Y$$
Assertion	drngmullcan	$$⊢\phi \to X=Y$$

Proof

Step	Hyp	Ref	Expression
1		drngmullcan.b	$$⊢B={\mathrm{Base}}_R$$
2		drngmullcan.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		drngmullcan.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		drngmullcan.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
5		drngmullcan.x	$$⊢\phi \to X\in B$$
6		drngmullcan.y	$$⊢\phi \to Y\in B$$
7		drngmullcan.z	$$⊢\phi \to Z\in B$$
8		drngmullcan.1	$$⊢\phi \to Z\ne \underset{\dot{}}{0}$$
9		drngmullcan.2	$$⊢\phi \to Z\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}Y$$
10	7 8	eldifsnd	$$⊢\phi \to Z\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
11		drngdomn	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{Domn}$$
12	4 11	syl	$$⊢\phi \to R\in \mathrm{Domn}$$
13	1 2 3 10 5 6 12 9	domnlcan	$$⊢\phi \to X=Y$$