Metamath Proof Explorer

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 ⊢ / = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 · ( 𝐼 ‘ 𝑦 ) ) )