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