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

Definition df-nsg 14635
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 14632 . 2  class NrmSGrp
2 vw . . 3  set  w
3 cgrp 14378 . . 3  class  Grp
4 vx . . . . . . . . . . . 12  set  x
54cv 1631 . . . . . . . . . . 11  class  x
6 vy . . . . . . . . . . . 12  set  y
76cv 1631 . . . . . . . . . . 11  class  y
8 vp . . . . . . . . . . . 12  set  p
98cv 1631 . . . . . . . . . . 11  class  p
105, 7, 9co 5874 . . . . . . . . . 10  class  ( x p y )
11 vs . . . . . . . . . . 11  set  s
1211cv 1631 . . . . . . . . . 10  class  s
1310, 12wcel 1696 . . . . . . . . 9  wff  ( x p y )  e.  s
147, 5, 9co 5874 . . . . . . . . . 10  class  ( y p x )
1514, 12wcel 1696 . . . . . . . . 9  wff  ( y p x )  e.  s
1613, 15wb 176 . . . . . . . 8  wff  ( ( x p y )  e.  s  <->  ( y
p x )  e.  s )
17 vb . . . . . . . . 9  set  b
1817cv 1631 . . . . . . . 8  class  b
1916, 6, 18wral 2556 . . . . . . 7  wff  A. y  e.  b  ( (
x p y )  e.  s  <->  ( y
p x )  e.  s )
2019, 4, 18wral 2556 . . . . . 6  wff  A. x  e.  b  A. y  e.  b  ( (
x p y )  e.  s  <->  ( y
p x )  e.  s )
212cv 1631 . . . . . . 7  class  w
22 cplusg 13224 . . . . . . 7  class  +g
2321, 22cfv 5271 . . . . . 6  class  ( +g  `  w )
2420, 8, 23wsbc 3004 . . . . 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 13164 . . . . . 6  class  Base
2621, 25cfv 5271 . . . . 5  class  ( Base `  w )
2724, 17, 26wsbc 3004 . . . 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 14631 . . . . 5  class SubGrp
2921, 28cfv 5271 . . . 4  class  (SubGrp `  w )
3027, 11, 29crab 2560 . . 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 4093 . 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 1632 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 set class
This definition is referenced by:  isnsg  14662
  Copyright terms: Public domain W3C validator