Theorem ringinvdv

Description: Write the inverse function in terms of division. (Contributed by Mario Carneiro, 2-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ringinvdv.b	$$⊢B={\mathrm{Base}}_R$$
2		ringinvdv.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
3		ringinvdv.d	$$⊢\underset{\dot{}}{\times }={/}_r\left(R\right)$$
4		ringinvdv.o	$$⊢\underset{\dot{}}{1}=1_R$$
5		ringinvdv.i	$$⊢I={inv}_r\left(R\right)$$
6	1 4	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
7		eqid	$$⊢{\cdot }_R={\cdot }_R$$
8	1 7 2 5 3	dvrval	$$⊢\left(\underset{\dot{}}{1}\in B\wedge X\in U\right)\to \underset{\dot{}}{1}\underset{\dot{}}{\times }X=\underset{\dot{}}{1}{\cdot }_{R}I\left(X\right)$$
9	6 8	sylan	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to \underset{\dot{}}{1}\underset{\dot{}}{\times }X=\underset{\dot{}}{1}{\cdot }_{R}I\left(X\right)$$
10	2 5 1	ringinvcl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to I\left(X\right)\in B$$
11	1 7 4	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge I\left(X\right)\in B\right)\to \underset{\dot{}}{1}{\cdot }_{R}I\left(X\right)=I\left(X\right)$$
12	10 11	syldan	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to \underset{\dot{}}{1}{\cdot }_{R}I\left(X\right)=I\left(X\right)$$
13	9 12	eqtr2d	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to I\left(X\right)=\underset{\dot{}}{1}\underset{\dot{}}{\times }X$$