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 = ( 𝑟 ∈ V , 𝑒 ∈ V ↦ ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ [ 𝑥 ] 𝑒 ) “s 𝑟 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cqus /s
1 vr 𝑟
2 cvv V
3 ve 𝑒
4 vx 𝑥
5 cbs Base
6 1 cv 𝑟
7 6 5 cfv ( Base ‘ 𝑟 )
8 4 cv 𝑥
9 3 cv 𝑒
10 8 9 cec [ 𝑥 ] 𝑒
11 4 7 10 cmpt ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ [ 𝑥 ] 𝑒 )
12 cimas s
13 11 6 12 co ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ [ 𝑥 ] 𝑒 ) “s 𝑟 )
14 1 3 2 2 13 cmpo ( 𝑟 ∈ V , 𝑒 ∈ V ↦ ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ [ 𝑥 ] 𝑒 ) “s 𝑟 ) )
15 0 14 wceq /s = ( 𝑟 ∈ V , 𝑒 ∈ V ↦ ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ [ 𝑥 ] 𝑒 ) “s 𝑟 ) )