Theorem dvr1

Description: A cancellation law for division. ( div1 analog.) (Contributed by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Hypotheses	dvr1.b	$$⊢B={\mathrm{Base}}_R$$
	dvr1.d	$$⊢\underset{\dot{}}{\times }={/}_r\left(R\right)$$
	dvr1.o	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	dvr1	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{\times }\underset{\dot{}}{1}=X$$

Proof

Step	Hyp	Ref	Expression
1		dvr1.b	$$⊢B={\mathrm{Base}}_R$$
2		dvr1.d	$$⊢\underset{\dot{}}{\times }={/}_r\left(R\right)$$
3		dvr1.o	$$⊢\underset{\dot{}}{1}=1_R$$
4		id	$$⊢X\in B\to X\in B$$
5		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
6	5 3	1unit	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in \mathrm{Unit}\left(R\right)$$
7		eqid	$$⊢{\cdot }_R={\cdot }_R$$
8		eqid	$$⊢{inv}_r\left(R\right)={inv}_r\left(R\right)$$
9	1 7 5 8 2	dvrval	$$⊢\left(X\in B\wedge \underset{\dot{}}{1}\in \mathrm{Unit}\left(R\right)\right)\to X\underset{\dot{}}{\times }\underset{\dot{}}{1}=X{\cdot }_R{inv}_r\left(R\right)\left(\underset{\dot{}}{1}\right)$$
10	4 6 9	syl2anr	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{\times }\underset{\dot{}}{1}=X{\cdot }_R{inv}_r\left(R\right)\left(\underset{\dot{}}{1}\right)$$
11	8 3	1rinv	$$⊢R\in \mathrm{Ring}\to {inv}_r\left(R\right)\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}$$
12	11	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to {inv}_r\left(R\right)\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}$$
13	12	oveq2d	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X{\cdot }_R{inv}_r\left(R\right)\left(\underset{\dot{}}{1}\right)=X{\cdot }_R\underset{\dot{}}{1}$$
14	1 7 3	ringridm	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X{\cdot }_R\underset{\dot{}}{1}=X$$
15	10 13 14	3eqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{\times }\underset{\dot{}}{1}=X$$