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

Definition df-nsg 14619
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 14616 . 2  class NrmSGrp
2 vw . . 3  set  w
3 cgrp 14362 . . 3  class  Grp
4 vx . . . . . . . . . . . 12  set  x
54cv 1622 . . . . . . . . . . 11  class  x
6 vy . . . . . . . . . . . 12  set  y
76cv 1622 . . . . . . . . . . 11  class  y
8 vp . . . . . . . . . . . 12  set  p
98cv 1622 . . . . . . . . . . 11  class  p
105, 7, 9co 5858 . . . . . . . . . 10  class  ( x p y )
11 vs . . . . . . . . . . 11  set  s
1211cv 1622 . . . . . . . . . 10  class  s
1310, 12wcel 1684 . . . . . . . . 9  wff  ( x p y )  e.  s
147, 5, 9co 5858 . . . . . . . . . 10  class  ( y p x )
1514, 12wcel 1684 . . . . . . . . 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 1622 . . . . . . . 8  class  b
1916, 6, 18wral 2543 . . . . . . 7  wff  A. y  e.  b  ( (
x p y )  e.  s  <->  ( y
p x )  e.  s )
2019, 4, 18wral 2543 . . . . . 6  wff  A. x  e.  b  A. y  e.  b  ( (
x p y )  e.  s  <->  ( y
p x )  e.  s )
212cv 1622 . . . . . . 7  class  w
22 cplusg 13208 . . . . . . 7  class  +g
2321, 22cfv 5255 . . . . . 6  class  ( +g  `  w )
2420, 8, 23wsbc 2991 . . . . 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 13148 . . . . . 6  class  Base
2621, 25cfv 5255 . . . . 5  class  ( Base `  w )
2724, 17, 26wsbc 2991 . . . 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 14615 . . . . 5  class SubGrp
2921, 28cfv 5255 . . . 4  class  (SubGrp `  w )
3027, 11, 29crab 2547 . . 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 4077 . 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 1623 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  14646
  Copyright terms: Public domain W3C validator