ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-eqg Unicode version

Definition df-eqg 12963
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
StepHypRef Expression
1 cqg 12960 . 2  class ~QG
2 vr . . 3  setvar  r
3 vi . . 3  setvar  i
4 cvv 2737 . . 3  class  _V
5 vx . . . . . . . 8  setvar  x
65cv 1352 . . . . . . 7  class  x
7 vy . . . . . . . 8  setvar  y
87cv 1352 . . . . . . 7  class  y
96, 8cpr 3593 . . . . . 6  class  { x ,  y }
102cv 1352 . . . . . . 7  class  r
11 cbs 12454 . . . . . . 7  class  Base
1210, 11cfv 5215 . . . . . 6  class  ( Base `  r )
139, 12wss 3129 . . . . 5  wff  { x ,  y }  C_  ( Base `  r )
14 cminusg 12810 . . . . . . . . 9  class  invg
1510, 14cfv 5215 . . . . . . . 8  class  ( invg `  r )
166, 15cfv 5215 . . . . . . 7  class  ( ( invg `  r
) `  x )
17 cplusg 12528 . . . . . . . 8  class  +g
1810, 17cfv 5215 . . . . . . 7  class  ( +g  `  r )
1916, 8, 18co 5872 . . . . . 6  class  ( ( ( invg `  r ) `  x
) ( +g  `  r
) y )
203cv 1352 . . . . . 6  class  i
2119, 20wcel 2148 . . . . 5  wff  ( ( ( invg `  r ) `  x
) ( +g  `  r
) y )  e.  i
2213, 21wa 104 . . . 4  wff  ( { x ,  y } 
C_  ( Base `  r
)  /\  ( (
( invg `  r ) `  x
) ( +g  `  r
) y )  e.  i )
2322, 5, 7copab 4062 . . 3  class  { <. x ,  y >.  |  ( { x ,  y }  C_  ( Base `  r )  /\  (
( ( invg `  r ) `  x
) ( +g  `  r
) y )  e.  i ) }
242, 3, 4, 4, 23cmpo 5874 . 2  class  ( r  e.  _V ,  i  e.  _V  |->  { <. x ,  y >.  |  ( { x ,  y }  C_  ( Base `  r )  /\  (
( ( invg `  r ) `  x
) ( +g  `  r
) y )  e.  i ) } )
251, 24wceq 1353 1  wff ~QG  =  ( r  e.  _V ,  i  e. 
_V  |->  { <. x ,  y >.  |  ( { x ,  y }  C_  ( Base `  r )  /\  (
( ( invg `  r ) `  x
) ( +g  `  r
) y )  e.  i ) } )
Colors of variables: wff set class
This definition is referenced by:  releqgg  13011  eqgfval  13012
  Copyright terms: Public domain W3C validator