Definition df-eqg 13378

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

Assertion

Ref	Expression
df-eqg	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )

Distinct variable group:   i, r, x, y

Detailed syntax breakdown of Definition df-eqg

Step	Hyp	Ref	Expression
1		cqg 13375	. 2 class ~QG
2		vr	. . 3 setvar r
3		vi	. . 3 setvar i
4		cvv 2763	. . 3 class _V
5		vx	. . . . . . . 8 setvar x
6	5	cv 1363	. . . . . . 7 class x
7		vy	. . . . . . . 8 setvar y
8	7	cv 1363	. . . . . . 7 class y
9	6, 8	cpr 3624	. . . . . 6 class { x , y }
10	2	cv 1363	. . . . . . 7 class r
11		cbs 12703	. . . . . . 7 class Base
12	10, 11	cfv 5259	. . . . . 6 class ( Base ` r )
13	9, 12	wss 3157	. . . . 5 wff { x , y } C_ ( Base ` r )
14		cminusg 13203	. . . . . . . . 9 class invg
15	10, 14	cfv 5259	. . . . . . . 8 class ( invg ` r )
16	6, 15	cfv 5259	. . . . . . 7 class ( ( invg ` r ) ` x )
17		cplusg 12780	. . . . . . . 8 class +g
18	10, 17	cfv 5259	. . . . . . 7 class ( +g ` r )
19	16, 8, 18	co 5925	. . . . . 6 class ( ( ( invg ` r ) ` x ) ( +g ` r ) y )
20	3	cv 1363	. . . . . 6 class i
21	19, 20	wcel 2167	. . . . 5 wff ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i
22	13, 21	wa 104	. . . 4 wff ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i )
23	22, 5, 7	copab 4094	. . 3 class { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) }
24	2, 3, 4, 4, 23	cmpo 5927	. 2 class ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
25	1, 24	wceq 1364	1 wff ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )

This definition is referenced by:  releqgg  13426  eqgex  13427  eqgfval  13428