Theorem drngmulrcan

Description: Cancellation of a nonzero factor on the right for multiplication. ( mulcan2ad 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}$$
	drngmulrcan.2	$$⊢\phi \to X\underset{\dot{}}{·}Z=Y\underset{\dot{}}{·}Z$$
Assertion	drngmulrcan	$$⊢\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		drngmulrcan.2	$$⊢\phi \to X\underset{\dot{}}{·}Z=Y\underset{\dot{}}{·}Z$$
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 5 6 10 12 9	domnrcan	$$⊢\phi \to X=Y$$