Theorem drngmulcan2ad

Description: Cancellation of a nonzero factor on the right for multiplication. ( mulcan2ad 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}$$
	drngmulcan2ad.2	$$⊢\phi \to X\underset{\dot{}}{·}Z=Y\underset{\dot{}}{·}Z$$
Assertion	drngmulcan2ad	$$⊢\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		drngmulcan2ad.2	$$⊢\phi \to X\underset{\dot{}}{·}Z=Y\underset{\dot{}}{·}Z$$
10	9	oveq1d	$$⊢\phi \to \left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}{inv}_r\left(R\right)\left(Z\right)=\left(Y\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}{inv}_r\left(R\right)\left(Z\right)$$
11	4	drngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
12		eqid	$$⊢{inv}_r\left(R\right)={inv}_r\left(R\right)$$
13	1 2 12 4 7 8	drnginvrcld	$$⊢\phi \to {inv}_r\left(R\right)\left(Z\right)\in B$$
14	1 3 11 5 7 13	ringassd	$$⊢\phi \to \left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}{inv}_r\left(R\right)\left(Z\right)=X\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}{inv}_r\left(R\right)\left(Z\right)\right)$$
15		eqid	$$⊢1_R=1_R$$
16	1 2 3 15 12 4 7 8	drnginvrrd	$$⊢\phi \to Z\underset{\dot{}}{·}{inv}_r\left(R\right)\left(Z\right)=1_R$$
17	16	oveq2d	$$⊢\phi \to X\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}{inv}_r\left(R\right)\left(Z\right)\right)=X\underset{\dot{}}{·}{1}_R$$
18	1 3 15 11 5	ringridmd	$$⊢\phi \to X\underset{\dot{}}{·}{1}_R=X$$
19	14 17 18	3eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}{inv}_r\left(R\right)\left(Z\right)=X$$
20	1 3 11 6 7 13	ringassd	$$⊢\phi \to \left(Y\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}{inv}_r\left(R\right)\left(Z\right)=Y\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}{inv}_r\left(R\right)\left(Z\right)\right)$$
21	16	oveq2d	$$⊢\phi \to Y\underset{\dot{}}{·}\left(Z\underset{\dot{}}{·}{inv}_r\left(R\right)\left(Z\right)\right)=Y\underset{\dot{}}{·}{1}_R$$
22	1 3 15 11 6	ringridmd	$$⊢\phi \to Y\underset{\dot{}}{·}{1}_R=Y$$
23	20 21 22	3eqtrd	$$⊢\phi \to \left(Y\underset{\dot{}}{·}Z\right)\underset{\dot{}}{·}{inv}_r\left(R\right)\left(Z\right)=Y$$
24	10 19 23	3eqtr3d	$$⊢\phi \to X=Y$$