This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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