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	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vi	$$setvari$$
4		vx	$$setvarx$$
5		vy	$$setvary$$
6	4	cv	$$setvarx$$
7	5	cv	$$setvary$$
8	6 7	cpr	$$class\left\{x,y\right\}$$
9		cbs	$$class\mathrm{Base}$$
10	1	cv	$$setvarr$$
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	$$setvari$$
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)$$