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