Theorem dvrid

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

	Ref	Expression
Hypotheses	unitdvcl.o	$$⊢U=\mathrm{Unit}\left(R\right)$$
	unitdvcl.d	$$⊢\underset{\dot{}}{\times }={/}_r\left(R\right)$$
	dvrid.o	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	dvrid	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to X\underset{\dot{}}{\times }X=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		unitdvcl.o	$$⊢U=\mathrm{Unit}\left(R\right)$$
2		unitdvcl.d	$$⊢\underset{\dot{}}{\times }={/}_r\left(R\right)$$
3		dvrid.o	$$⊢\underset{\dot{}}{1}=1_R$$
4		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
5	4 1	unitcl	$$⊢X\in U\to X\in {\mathrm{Base}}_R$$
6	5	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to X\in {\mathrm{Base}}_R$$
7		eqid	$$⊢{\cdot }_R={\cdot }_R$$
8		eqid	$$⊢{inv}_r\left(R\right)={inv}_r\left(R\right)$$
9	4 7 1 8 2	dvrval	$$⊢\left(X\in {\mathrm{Base}}_R\wedge X\in U\right)\to X\underset{\dot{}}{\times }X=X{\cdot }_R{inv}_r\left(R\right)\left(X\right)$$
10	6 9	sylancom	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to X\underset{\dot{}}{\times }X=X{\cdot }_R{inv}_r\left(R\right)\left(X\right)$$
11	1 8 7 3	unitrinv	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to X{\cdot }_R{inv}_r\left(R\right)\left(X\right)=\underset{\dot{}}{1}$$
12	10 11	eqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to X\underset{\dot{}}{\times }X=\underset{\dot{}}{1}$$