# Metamath Proof Explorer

## Definition df-eqg

Description: Define the equivalence relation in a group generated by a subgroup. More precisely, if G is a group and H is a subgroup, then G ~QG H is the equivalence relation on G associated with the left cosets of H . A typical application of this definition is the construction of the quotient group (resp. ring) of a group (resp. ring) by a normal subgroup (resp. two-sided ideal). (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Assertion df-eqg ${⊢}{~}_{\mathit{QG}}=\left({r}\in \mathrm{V},{i}\in \mathrm{V}⟼\left\{⟨{x},{y}⟩|\left(\left\{{x},{y}\right\}\subseteq {\mathrm{Base}}_{{r}}\wedge {inv}_{g}\left({r}\right)\left({x}\right){+}_{{r}}{y}\in {i}\right)\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cqg ${class}{~}_{\mathit{QG}}$
1 vr ${setvar}{r}$
2 cvv ${class}\mathrm{V}$
3 vi ${setvar}{i}$
4 vx ${setvar}{x}$
5 vy ${setvar}{y}$
6 4 cv ${setvar}{x}$
7 5 cv ${setvar}{y}$
8 6 7 cpr ${class}\left\{{x},{y}\right\}$
9 cbs ${class}\mathrm{Base}$
10 1 cv ${setvar}{r}$
11 10 9 cfv ${class}{\mathrm{Base}}_{{r}}$
12 8 11 wss ${wff}\left\{{x},{y}\right\}\subseteq {\mathrm{Base}}_{{r}}$
13 cminusg ${class}{inv}_{g}$
14 10 13 cfv ${class}{inv}_{g}\left({r}\right)$
15 6 14 cfv ${class}{inv}_{g}\left({r}\right)\left({x}\right)$
16 cplusg ${class}{+}_{𝑔}$
17 10 16 cfv ${class}{+}_{{r}}$
18 15 7 17 co ${class}\left({inv}_{g}\left({r}\right)\left({x}\right){+}_{{r}}{y}\right)$
19 3 cv ${setvar}{i}$
20 18 19 wcel ${wff}{inv}_{g}\left({r}\right)\left({x}\right){+}_{{r}}{y}\in {i}$
21 12 20 wa ${wff}\left(\left\{{x},{y}\right\}\subseteq {\mathrm{Base}}_{{r}}\wedge {inv}_{g}\left({r}\right)\left({x}\right){+}_{{r}}{y}\in {i}\right)$
22 21 4 5 copab ${class}\left\{⟨{x},{y}⟩|\left(\left\{{x},{y}\right\}\subseteq {\mathrm{Base}}_{{r}}\wedge {inv}_{g}\left({r}\right)\left({x}\right){+}_{{r}}{y}\in {i}\right)\right\}$
23 1 3 2 2 22 cmpo ${class}\left({r}\in \mathrm{V},{i}\in \mathrm{V}⟼\left\{⟨{x},{y}⟩|\left(\left\{{x},{y}\right\}\subseteq {\mathrm{Base}}_{{r}}\wedge {inv}_{g}\left({r}\right)\left({x}\right){+}_{{r}}{y}\in {i}\right)\right\}\right)$
24 0 23 wceq ${wff}{~}_{\mathit{QG}}=\left({r}\in \mathrm{V},{i}\in \mathrm{V}⟼\left\{⟨{x},{y}⟩|\left(\left\{{x},{y}\right\}\subseteq {\mathrm{Base}}_{{r}}\wedge {inv}_{g}\left({r}\right)\left({x}\right){+}_{{r}}{y}\in {i}\right)\right\}\right)$