Metamath Proof Explorer


Definition df-nsg

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)

Ref Expression
Assertion 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 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnsg
 |-  NrmSGrp
1 vw
 |-  w
2 cgrp
 |-  Grp
3 vs
 |-  s
4 csubg
 |-  SubGrp
5 1 cv
 |-  w
6 5 4 cfv
 |-  ( SubGrp ` w )
7 cbs
 |-  Base
8 5 7 cfv
 |-  ( Base ` w )
9 vb
 |-  b
10 cplusg
 |-  +g
11 5 10 cfv
 |-  ( +g ` w )
12 vp
 |-  p
13 vx
 |-  x
14 9 cv
 |-  b
15 vy
 |-  y
16 13 cv
 |-  x
17 12 cv
 |-  p
18 15 cv
 |-  y
19 16 18 17 co
 |-  ( x p y )
20 3 cv
 |-  s
21 19 20 wcel
 |-  ( x p y ) e. s
22 18 16 17 co
 |-  ( y p x )
23 22 20 wcel
 |-  ( y p x ) e. s
24 21 23 wb
 |-  ( ( x p y ) e. s <-> ( y p x ) e. s )
25 24 15 14 wral
 |-  A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s )
26 25 13 14 wral
 |-  A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s )
27 26 12 11 wsbc
 |-  [. ( +g ` w ) / p ]. A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s )
28 27 9 8 wsbc
 |-  [. ( Base ` w ) / b ]. [. ( +g ` w ) / p ]. A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s )
29 28 3 6 crab
 |-  { 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 ) }
30 1 2 29 cmpt
 |-  ( 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 ) } )
31 0 30 wceq
 |-  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 ) } )