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

Definition df-divs 13737
Description: Define a quotient ring (or quotient group), which is a special case of an image structure df-imas 13736 where the image function is  x  |->  [ x ] e. (Contributed by Mario Carneiro, 23-Feb-2015.)
Assertion
Ref Expression
df-divs  |-  /.s  =  (
r  e.  _V , 
e  e.  _V  |->  ( ( x  e.  (
Base `  r )  |->  [ x ] e )  "s  r ) )
Distinct variable group:    e, r, x

Detailed syntax breakdown of Definition df-divs
StepHypRef Expression
1 cqus 13733 . 2  class  /.s
2 vr . . 3  set  r
3 ve . . 3  set  e
4 cvv 2958 . . 3  class  _V
5 vx . . . . 5  set  x
62cv 1652 . . . . . 6  class  r
7 cbs 13471 . . . . . 6  class  Base
86, 7cfv 5456 . . . . 5  class  ( Base `  r )
95cv 1652 . . . . . 6  class  x
103cv 1652 . . . . . 6  class  e
119, 10cec 6905 . . . . 5  class  [ x ] e
125, 8, 11cmpt 4268 . . . 4  class  ( x  e.  ( Base `  r
)  |->  [ x ]
e )
13 cimas 13732 . . . 4  class  "s
1412, 6, 13co 6083 . . 3  class  ( ( x  e.  ( Base `  r )  |->  [ x ] e )  "s  r
)
152, 3, 4, 4, 14cmpt2 6085 . 2  class  ( r  e.  _V ,  e  e.  _V  |->  ( ( x  e.  ( Base `  r )  |->  [ x ] e )  "s  r
) )
161, 15wceq 1653 1  wff  /.s  =  (
r  e.  _V , 
e  e.  _V  |->  ( ( x  e.  (
Base `  r )  |->  [ x ] e )  "s  r ) )
Colors of variables: wff set class
This definition is referenced by:  divsval  13769
  Copyright terms: Public domain W3C validator