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 ) } )