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 ⊢ / 𝑠 = r ∈ V , e ∈ V ⟼ x ∈ Base r ⟼ x e “ 𝑠 r

Detailed syntax breakdown

Step Hyp Ref Expression
0 cqus class / 𝑠
1 vr setvar r
2 cvv class V
3 ve setvar e
4 vx setvar x
5 cbs class Base
6 1 cv setvar r
7 6 5 cfv class Base r
8 4 cv setvar x
9 3 cv setvar e
10 8 9 cec class x e
11 4 7 10 cmpt class x ∈ Base r ⟼ x e
12 cimas class “ 𝑠
13 11 6 12 co class x ∈ Base r ⟼ x e “ 𝑠 r
14 1 3 2 2 13 cmpo class r ∈ V , e ∈ V ⟼ x ∈ Base r ⟼ x e “ 𝑠 r
15 0 14 wceq wff / 𝑠 = r ∈ V , e ∈ V ⟼ x ∈ Base r ⟼ x e “ 𝑠 r