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	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cqg	|- ~QG
1		vr	|- r
2		cvv	|- _V
3		vi	|- i
4		vx	|- x
5		vy	|- y
6	4	cv	|- x
7	5	cv	|- y
8	6 7	cpr	|- { x , y }
9		cbs	|- Base
10	1	cv	|- r
11	10 9	cfv	|- ( Base ` r )
12	8 11	wss	|- { x , y } C_ ( Base ` r )
13		cminusg	|- invg
14	10 13	cfv	|- ( invg ` r )
15	6 14	cfv	|- ( ( invg ` r ) ` x )
16		cplusg	|- +g
17	10 16	cfv	|- ( +g ` r )
18	15 7 17	co	|- ( ( ( invg ` r ) ` x ) ( +g ` r ) y )
19	3	cv	|- i
20	18 19	wcel	|- ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i
21	12 20	wa	|- ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i )
22	21 4 5	copab	|- { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) }
23	1 3 2 2 22	cmpo	|- ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )
24	0 23	wceq	|- ~QG = ( r e. _V , i e. _V |-> { <. x , y >. | ( { x , y } C_ ( Base ` r ) /\ ( ( ( invg ` r ) ` x ) ( +g ` r ) y ) e. i ) } )