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

Definition df-dvr 15481
Description: Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.)
Assertion
Ref Expression
df-dvr  |- /r  =  (
r  e.  _V  |->  ( x  e.  ( Base `  r ) ,  y  e.  (Unit `  r
)  |->  ( x ( .r `  r ) ( ( invr `  r
) `  y )
) ) )
Distinct variable group:    x, r, y

Detailed syntax breakdown of Definition df-dvr
StepHypRef Expression
1 cdvr 15480 . 2  class /r
2 vr . . 3  set  r
3 cvv 2801 . . 3  class  _V
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1631 . . . . 5  class  r
7 cbs 13164 . . . . 5  class  Base
86, 7cfv 5271 . . . 4  class  ( Base `  r )
9 cui 15437 . . . . 5  class Unit
106, 9cfv 5271 . . . 4  class  (Unit `  r )
114cv 1631 . . . . 5  class  x
125cv 1631 . . . . . 6  class  y
13 cinvr 15469 . . . . . . 7  class  invr
146, 13cfv 5271 . . . . . 6  class  ( invr `  r )
1512, 14cfv 5271 . . . . 5  class  ( (
invr `  r ) `  y )
16 cmulr 13225 . . . . . 6  class  .r
176, 16cfv 5271 . . . . 5  class  ( .r
`  r )
1811, 15, 17co 5874 . . . 4  class  ( x ( .r `  r
) ( ( invr `  r ) `  y
) )
194, 5, 8, 10, 18cmpt2 5876 . . 3  class  ( x  e.  ( Base `  r
) ,  y  e.  (Unit `  r )  |->  ( x ( .r
`  r ) ( ( invr `  r
) `  y )
) )
202, 3, 19cmpt 4093 . 2  class  ( r  e.  _V  |->  ( x  e.  ( Base `  r
) ,  y  e.  (Unit `  r )  |->  ( x ( .r
`  r ) ( ( invr `  r
) `  y )
) ) )
211, 20wceq 1632 1  wff /r  =  (
r  e.  _V  |->  ( x  e.  ( Base `  r ) ,  y  e.  (Unit `  r
)  |->  ( x ( .r `  r ) ( ( invr `  r
) `  y )
) ) )
Colors of variables: wff set class
This definition is referenced by:  dvrfval  15482
  Copyright terms: Public domain W3C validator