Theorem dvrval

Description: Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014) (Revised by Mario Carneiro, 2-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dvrval.b	$$⊢B={\mathrm{Base}}_R$$
2		dvrval.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		dvrval.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
4		dvrval.i	$$⊢I={inv}_r\left(R\right)$$
5		dvrval.d	$$⊢\underset{\dot{}}{\times }={/}_r\left(R\right)$$
6		oveq1	$$⊢x=X\to x\underset{\dot{}}{·}I\left(y\right)=X\underset{\dot{}}{·}I\left(y\right)$$
7		fveq2	$$⊢y=Y\to I\left(y\right)=I\left(Y\right)$$
8	7	oveq2d	$$⊢y=Y\to X\underset{\dot{}}{·}I\left(y\right)=X\underset{\dot{}}{·}I\left(Y\right)$$
9	1 2 3 4 5	dvrfval	$$⊢\underset{\dot{}}{\times }=\left(x\in B,y\in U⟼x\underset{\dot{}}{·}I\left(y\right)\right)$$
10		ovex	$$⊢X\underset{\dot{}}{·}I\left(Y\right)\in \mathrm{V}$$
11	6 8 9 10	ovmpo	$$⊢\left(X\in B\wedge Y\in U\right)\to X\underset{\dot{}}{\times }Y=X\underset{\dot{}}{·}I\left(Y\right)$$