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
|- ~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 ) } )