Theorem drngmulcanad

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

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

Proof

Step	Hyp	Ref	Expression
1		drngmulcanad.b	$$⊢B={\mathrm{Base}}_R$$
2		drngmulcanad.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		drngmulcanad.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		drngmulcanad.r	$$⊢\phi \to R\in \mathrm{DivRing}$$
5		drngmulcanad.x	$$⊢\phi \to X\in B$$
6		drngmulcanad.y	$$⊢\phi \to Y\in B$$
7		drngmulcanad.z	$$⊢\phi \to Z\in B$$
8		drngmulcanad.1	$$⊢\phi \to Z\ne \underset{\dot{}}{0}$$
9		drngmulcanad.2	$$⊢\phi \to Z\underset{\dot{}}{·}X=Z\underset{\dot{}}{·}Y$$
10	9	oveq2d	$$⊢\phi \to {inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}X\right)={inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}Y\right)$$
11		eqid	$$⊢1_R=1_R$$
12		eqid	$$⊢{inv}_r\left(R\right)={inv}_r\left(R\right)$$
13	1 2 3 11 12 4 7 8	drnginvrld	$$⊢\phi \to {inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}Z=1_R$$
14	13	oveq1d	$$⊢\phi \to \left({inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}X=1_R\underset{\dot{}}{·}X$$
15	4	drngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
16	1 2 12 4 7 8	drnginvrcld	$$⊢\phi \to {inv}_r\left(R\right)\left(Z\right)\in B$$
17	1 3 15 16 7 5	ringassd	$$⊢\phi \to \left({inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}X={inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}X\right)$$
18	1 3 11 15 5	ringlidmd	$$⊢\phi \to 1_R\underset{\dot{}}{·}X=X$$
19	14 17 18	3eqtr3d	$$⊢\phi \to {inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}X\right)=X$$
20	13	oveq1d	$$⊢\phi \to \left({inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}Y=1_R\underset{\dot{}}{·}Y$$
21	1 3 15 16 7 6	ringassd	$$⊢\phi \to \left({inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}Y={inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}Y\right)$$
22	1 3 11 15 6	ringlidmd	$$⊢\phi \to 1_R\underset{\dot{}}{·}Y=Y$$
23	20 21 22	3eqtr3d	$$⊢\phi \to {inv}_r\left(R\right)\left(Z\right)\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}Y\right)=Y$$
24	10 19 23	3eqtr3d	$$⊢\phi \to X=Y$$