MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-eqg Unicode version

Definition df-eqg 14620
Description: Define the equivalence relation in a quotient ring or quotient group (where  i is a two-sided ideal or a normal subgroup). For non-normal subgroups this generates the left cosets. (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 )  /\  (
( ( inv g `  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 14617 . 2  class ~QG
2 vr . . 3  set  r
3 vi . . 3  set  i
4 cvv 2788 . . 3  class  _V
5 vx . . . . . . . 8  set  x
65cv 1622 . . . . . . 7  class  x
7 vy . . . . . . . 8  set  y
87cv 1622 . . . . . . 7  class  y
96, 8cpr 3641 . . . . . 6  class  { x ,  y }
102cv 1622 . . . . . . 7  class  r
11 cbs 13148 . . . . . . 7  class  Base
1210, 11cfv 5255 . . . . . 6  class  ( Base `  r )
139, 12wss 3152 . . . . 5  wff  { x ,  y }  C_  ( Base `  r )
14 cminusg 14363 . . . . . . . . 9  class  inv g
1510, 14cfv 5255 . . . . . . . 8  class  ( inv g `  r )
166, 15cfv 5255 . . . . . . 7  class  ( ( inv g `  r
) `  x )
17 cplusg 13208 . . . . . . . 8  class  +g
1810, 17cfv 5255 . . . . . . 7  class  ( +g  `  r )
1916, 8, 18co 5858 . . . . . 6  class  ( ( ( inv g `  r ) `  x
) ( +g  `  r
) y )
203cv 1622 . . . . . 6  class  i
2119, 20wcel 1684 . . . . 5  wff  ( ( ( inv g `  r ) `  x
) ( +g  `  r
) y )  e.  i
2213, 21wa 358 . . . 4  wff  ( { x ,  y } 
C_  ( Base `  r
)  /\  ( (
( inv g `  r ) `  x
) ( +g  `  r
) y )  e.  i )
2322, 5, 7copab 4076 . . 3  class  { <. x ,  y >.  |  ( { x ,  y }  C_  ( Base `  r )  /\  (
( ( inv g `  r ) `  x
) ( +g  `  r
) y )  e.  i ) }
242, 3, 4, 4, 23cmpt2 5860 . 2  class  ( r  e.  _V ,  i  e.  _V  |->  { <. x ,  y >.  |  ( { x ,  y }  C_  ( Base `  r )  /\  (
( ( inv g `  r ) `  x
) ( +g  `  r
) y )  e.  i ) } )
251, 24wceq 1623 1  wff ~QG  =  ( r  e.  _V ,  i  e. 
_V  |->  { <. x ,  y >.  |  ( { x ,  y }  C_  ( Base `  r )  /\  (
( ( inv g `  r ) `  x
) ( +g  `  r
) y )  e.  i ) } )
Colors of variables: wff set class
This definition is referenced by:  releqg  14664  eqgfval  14665
  Copyright terms: Public domain W3C validator