Metamath Proof Explorer


Definition df-qus

Description: Define a quotient ring (or quotient group), which is a special case of an image structure df-imas where the image function is x |-> [ x ] e . (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Assertion df-qus
|- /s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cqus
 |-  /s
1 vr
 |-  r
2 cvv
 |-  _V
3 ve
 |-  e
4 vx
 |-  x
5 cbs
 |-  Base
6 1 cv
 |-  r
7 6 5 cfv
 |-  ( Base ` r )
8 4 cv
 |-  x
9 3 cv
 |-  e
10 8 9 cec
 |-  [ x ] e
11 4 7 10 cmpt
 |-  ( x e. ( Base ` r ) |-> [ x ] e )
12 cimas
 |-  "s
13 11 6 12 co
 |-  ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r )
14 1 3 2 2 13 cmpo
 |-  ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
15 0 14 wceq
 |-  /s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )