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

Definition df-dvr 15793
 Description: Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.)
Assertion
Ref Expression
df-dvr /r Unit
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-dvr
StepHypRef Expression
1 cdvr 15792 . 2 /r
2 vr . . 3
3 cvv 2958 . . 3
4 vx . . . 4
5 vy . . . 4
62cv 1652 . . . . 5
7 cbs 13474 . . . . 5
86, 7cfv 5457 . . . 4
9 cui 15749 . . . . 5 Unit
106, 9cfv 5457 . . . 4 Unit
114cv 1652 . . . . 5
125cv 1652 . . . . . 6
13 cinvr 15781 . . . . . . 7
146, 13cfv 5457 . . . . . 6
1512, 14cfv 5457 . . . . 5
16 cmulr 13535 . . . . . 6
176, 16cfv 5457 . . . . 5
1811, 15, 17co 6084 . . . 4
194, 5, 8, 10, 18cmpt2 6086 . . 3 Unit
202, 3, 19cmpt 4269 . 2 Unit
211, 20wceq 1653 1 /r Unit
 Colors of variables: wff set class This definition is referenced by:  dvrfval  15794
 Copyright terms: Public domain W3C validator