Theorem dvrfval

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

	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	dvrfval	$$⊢\underset{\dot{}}{\times }=\left(x\in B,y\in U⟼x\underset{\dot{}}{·}I\left(y\right)\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		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
7	6 1	eqtr4di	$$⊢r=R\to {\mathrm{Base}}_r=B$$
8		fveq2	$$⊢r=R\to \mathrm{Unit}\left(r\right)=\mathrm{Unit}\left(R\right)$$
9	8 3	eqtr4di	$$⊢r=R\to \mathrm{Unit}\left(r\right)=U$$
10		fveq2	$$⊢r=R\to {\cdot }_r={\cdot }_R$$
11	10 2	eqtr4di	$$⊢r=R\to {\cdot }_r=\underset{\dot{}}{·}$$
12		eqidd	$$⊢r=R\to x=x$$
13		fveq2	$$⊢r=R\to {inv}_r\left(r\right)={inv}_r\left(R\right)$$
14	13 4	eqtr4di	$$⊢r=R\to {inv}_r\left(r\right)=I$$
15	14	fveq1d	$$⊢r=R\to {inv}_r\left(r\right)\left(y\right)=I\left(y\right)$$
16	11 12 15	oveq123d	$$⊢r=R\to x{\cdot }_r{inv}_r\left(r\right)\left(y\right)=x\underset{\dot{}}{·}I\left(y\right)$$
17	7 9 16	mpoeq123dv	$$⊢r=R\to \left(x\in {\mathrm{Base}}_r,y\in \mathrm{Unit}\left(r\right)⟼x{\cdot }_r{inv}_r\left(r\right)\left(y\right)\right)=\left(x\in B,y\in U⟼x\underset{\dot{}}{·}I\left(y\right)\right)$$
18		df-dvr	$$⊢{/}_r=\left(r\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_r,y\in \mathrm{Unit}\left(r\right)⟼x{\cdot }_r{inv}_r\left(r\right)\left(y\right)\right)\right)$$
19	1	fvexi	$$⊢B\in \mathrm{V}$$
20	3	fvexi	$$⊢U\in \mathrm{V}$$
21	19 20	mpoex	$$⊢\left(x\in B,y\in U⟼x\underset{\dot{}}{·}I\left(y\right)\right)\in \mathrm{V}$$
22	17 18 21	fvmpt	$$⊢R\in \mathrm{V}\to {/}_r\left(R\right)=\left(x\in B,y\in U⟼x\underset{\dot{}}{·}I\left(y\right)\right)$$
23		fvprc	$$⊢\neg R\in \mathrm{V}\to {/}_r\left(R\right)=\varnothing$$
24		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Base}}_R=\varnothing$$
25	1 24	syl5eq	$$⊢\neg R\in \mathrm{V}\to B=\varnothing$$
26	25	orcd	$$⊢\neg R\in \mathrm{V}\to \left(B=\varnothing \vee U=\varnothing \right)$$
27		0mpo0	$$⊢\left(B=\varnothing \vee U=\varnothing \right)\to \left(x\in B,y\in U⟼x\underset{\dot{}}{·}I\left(y\right)\right)=\varnothing$$
28	26 27	syl	$$⊢\neg R\in \mathrm{V}\to \left(x\in B,y\in U⟼x\underset{\dot{}}{·}I\left(y\right)\right)=\varnothing$$
29	23 28	eqtr4d	$$⊢\neg R\in \mathrm{V}\to {/}_r\left(R\right)=\left(x\in B,y\in U⟼x\underset{\dot{}}{·}I\left(y\right)\right)$$
30	22 29	pm2.61i	$$⊢{/}_r\left(R\right)=\left(x\in B,y\in U⟼x\underset{\dot{}}{·}I\left(y\right)\right)$$
31	5 30	eqtri	$$⊢\underset{\dot{}}{\times }=\left(x\in B,y\in U⟼x\underset{\dot{}}{·}I\left(y\right)\right)$$