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 ) ) |
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 ) ) |