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

Definition df-nsg 15691
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-nsg  |- NrmSGrp  =  ( w  e.  Grp  |->  { s  e.  (SubGrp `  w )  |  [. ( Base `  w )  /  b ]. [. ( +g  `  w )  /  p ]. A. x  e.  b  A. y  e.  b  ( ( x p y )  e.  s  <->  ( y p x )  e.  s ) } )
Distinct variable group:    p, b, s, w, x, y

Detailed syntax breakdown of Definition df-nsg
StepHypRef Expression
1 cnsg 15688 . 2  class NrmSGrp
2 vw . . 3  setvar  w
3 cgrp 15422 . . 3  class  Grp
4 vx . . . . . . . . . . . 12  setvar  x
54cv 1368 . . . . . . . . . . 11  class  x
6 vy . . . . . . . . . . . 12  setvar  y
76cv 1368 . . . . . . . . . . 11  class  y
8 vp . . . . . . . . . . . 12  setvar  p
98cv 1368 . . . . . . . . . . 11  class  p
105, 7, 9co 6103 . . . . . . . . . 10  class  ( x p y )
11 vs . . . . . . . . . . 11  setvar  s
1211cv 1368 . . . . . . . . . 10  class  s
1310, 12wcel 1756 . . . . . . . . 9  wff  ( x p y )  e.  s
147, 5, 9co 6103 . . . . . . . . . 10  class  ( y p x )
1514, 12wcel 1756 . . . . . . . . 9  wff  ( y p x )  e.  s
1613, 15wb 184 . . . . . . . 8  wff  ( ( x p y )  e.  s  <->  ( y
p x )  e.  s )
17 vb . . . . . . . . 9  setvar  b
1817cv 1368 . . . . . . . 8  class  b
1916, 6, 18wral 2727 . . . . . . 7  wff  A. y  e.  b  ( (
x p y )  e.  s  <->  ( y
p x )  e.  s )
2019, 4, 18wral 2727 . . . . . 6  wff  A. x  e.  b  A. y  e.  b  ( (
x p y )  e.  s  <->  ( y
p x )  e.  s )
212cv 1368 . . . . . . 7  class  w
22 cplusg 14250 . . . . . . 7  class  +g
2321, 22cfv 5430 . . . . . 6  class  ( +g  `  w )
2420, 8, 23wsbc 3198 . . . . 5  wff  [. ( +g  `  w )  /  p ]. A. x  e.  b  A. y  e.  b  ( ( x p y )  e.  s  <->  ( y p x )  e.  s )
25 cbs 14186 . . . . . 6  class  Base
2621, 25cfv 5430 . . . . 5  class  ( Base `  w )
2724, 17, 26wsbc 3198 . . . 4  wff  [. ( Base `  w )  / 
b ]. [. ( +g  `  w )  /  p ]. A. x  e.  b 
A. y  e.  b  ( ( x p y )  e.  s  <-> 
( y p x )  e.  s )
28 csubg 15687 . . . . 5  class SubGrp
2921, 28cfv 5430 . . . 4  class  (SubGrp `  w )
3027, 11, 29crab 2731 . . 3  class  { s  e.  (SubGrp `  w
)  |  [. ( Base `  w )  / 
b ]. [. ( +g  `  w )  /  p ]. A. x  e.  b 
A. y  e.  b  ( ( x p y )  e.  s  <-> 
( y p x )  e.  s ) }
312, 3, 30cmpt 4362 . 2  class  ( w  e.  Grp  |->  { s  e.  (SubGrp `  w
)  |  [. ( Base `  w )  / 
b ]. [. ( +g  `  w )  /  p ]. A. x  e.  b 
A. y  e.  b  ( ( x p y )  e.  s  <-> 
( y p x )  e.  s ) } )
321, 31wceq 1369 1  wff NrmSGrp  =  ( w  e.  Grp  |->  { s  e.  (SubGrp `  w )  |  [. ( Base `  w )  /  b ]. [. ( +g  `  w )  /  p ]. A. x  e.  b  A. y  e.  b  ( ( x p y )  e.  s  <->  ( y p x )  e.  s ) } )
Colors of variables: wff setvar class
This definition is referenced by:  isnsg  15722
  Copyright terms: Public domain W3C validator