MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dvr Structured version   Visualization version   GIF version

Definition df-dvr 18885
Description: Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.)
Assertion
Ref Expression
df-dvr /r = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r𝑟)((invr𝑟)‘𝑦))))
Distinct variable group:   𝑥,𝑟,𝑦

Detailed syntax breakdown of Definition df-dvr
StepHypRef Expression
1 cdvr 18884 . 2 class /r
2 vr . . 3 setvar 𝑟
3 cvv 3391 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1636 . . . . 5 class 𝑟
7 cbs 16068 . . . . 5 class Base
86, 7cfv 6101 . . . 4 class (Base‘𝑟)
9 cui 18841 . . . . 5 class Unit
106, 9cfv 6101 . . . 4 class (Unit‘𝑟)
114cv 1636 . . . . 5 class 𝑥
125cv 1636 . . . . . 6 class 𝑦
13 cinvr 18873 . . . . . . 7 class invr
146, 13cfv 6101 . . . . . 6 class (invr𝑟)
1512, 14cfv 6101 . . . . 5 class ((invr𝑟)‘𝑦)
16 cmulr 16154 . . . . . 6 class .r
176, 16cfv 6101 . . . . 5 class (.r𝑟)
1811, 15, 17co 6874 . . . 4 class (𝑥(.r𝑟)((invr𝑟)‘𝑦))
194, 5, 8, 10, 18cmpt2 6876 . . 3 class (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r𝑟)((invr𝑟)‘𝑦)))
202, 3, 19cmpt 4923 . 2 class (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r𝑟)((invr𝑟)‘𝑦))))
211, 20wceq 1637 1 wff /r = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟), 𝑦 ∈ (Unit‘𝑟) ↦ (𝑥(.r𝑟)((invr𝑟)‘𝑦))))
Colors of variables: wff setvar class
This definition is referenced by:  dvrfval  18886
  Copyright terms: Public domain W3C validator