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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	dvrval.t	⊢ · = ( .r ‘ 𝑅 )
	dvrval.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	dvrval.i	⊢ 𝐼 = ( invr ‘ 𝑅 )
	dvrval.d	⊢ / = ( /r ‘ 𝑅 )
Assertion	dvrfval	⊢ / = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 · ( 𝐼 ‘ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvrval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		dvrval.t	⊢ · = ( .r ‘ 𝑅 )
3		dvrval.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
4		dvrval.i	⊢ 𝐼 = ( invr ‘ 𝑅 )
5		dvrval.d	⊢ / = ( /r ‘ 𝑅 )
6		fveq2	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
7	6 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
8		fveq2	⊢ ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = ( Unit ‘ 𝑅 ) )
9	8 3	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = 𝑈 )
10		fveq2	⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
11	10 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = · )
12		eqidd	⊢ ( 𝑟 = 𝑅 → 𝑥 = 𝑥 )
13		fveq2	⊢ ( 𝑟 = 𝑅 → ( invr ‘ 𝑟 ) = ( invr ‘ 𝑅 ) )
14	13 4	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( invr ‘ 𝑟 ) = 𝐼 )
15	14	fveq1d	⊢ ( 𝑟 = 𝑅 → ( ( invr ‘ 𝑟 ) ‘ 𝑦 ) = ( 𝐼 ‘ 𝑦 ) )
16	11 12 15	oveq123d	⊢ ( 𝑟 = 𝑅 → ( 𝑥 ( .r ‘ 𝑟 ) ( ( invr ‘ 𝑟 ) ‘ 𝑦 ) ) = ( 𝑥 · ( 𝐼 ‘ 𝑦 ) ) )
17	7 9 16	mpoeq123dv	⊢ ( 𝑟 = 𝑅 → ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Unit ‘ 𝑟 ) ↦ ( 𝑥 ( .r ‘ 𝑟 ) ( ( invr ‘ 𝑟 ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 · ( 𝐼 ‘ 𝑦 ) ) ) )
18		df-dvr	⊢ /r = ( 𝑟 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑟 ) , 𝑦 ∈ ( Unit ‘ 𝑟 ) ↦ ( 𝑥 ( .r ‘ 𝑟 ) ( ( invr ‘ 𝑟 ) ‘ 𝑦 ) ) ) )
19	1	fvexi	⊢ 𝐵 ∈ V
20	3	fvexi	⊢ 𝑈 ∈ V
21	19 20	mpoex	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 · ( 𝐼 ‘ 𝑦 ) ) ) ∈ V
22	17 18 21	fvmpt	⊢ ( 𝑅 ∈ V → ( /r ‘ 𝑅 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 · ( 𝐼 ‘ 𝑦 ) ) ) )
23		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( /r ‘ 𝑅 ) = ∅ )
24		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ 𝑅 ) = ∅ )
25	1 24	eqtrid	⊢ ( ¬ 𝑅 ∈ V → 𝐵 = ∅ )
26	25	orcd	⊢ ( ¬ 𝑅 ∈ V → ( 𝐵 = ∅ ∨ 𝑈 = ∅ ) )
27		0mpo0	⊢ ( ( 𝐵 = ∅ ∨ 𝑈 = ∅ ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 · ( 𝐼 ‘ 𝑦 ) ) ) = ∅ )
28	26 27	syl	⊢ ( ¬ 𝑅 ∈ V → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 · ( 𝐼 ‘ 𝑦 ) ) ) = ∅ )
29	23 28	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → ( /r ‘ 𝑅 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 · ( 𝐼 ‘ 𝑦 ) ) ) )
30	22 29	pm2.61i	⊢ ( /r ‘ 𝑅 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 · ( 𝐼 ‘ 𝑦 ) ) )
31	5 30	eqtri	⊢ / = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 · ( 𝐼 ‘ 𝑦 ) ) )