Definition df-nsg 13301

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

Step	Hyp	Ref	Expression
1		cnsg 13298	. 2 class NrmSGrp
2		vw	. . 3 setvar w
3		cgrp 13132	. . 3 class Grp
4		vx	. . . . . . . . . . . 12 setvar x
5	4	cv 1363	. . . . . . . . . . 11 class x
6		vy	. . . . . . . . . . . 12 setvar y
7	6	cv 1363	. . . . . . . . . . 11 class y
8		vp	. . . . . . . . . . . 12 setvar p
9	8	cv 1363	. . . . . . . . . . 11 class p
10	5, 7, 9	co 5922	. . . . . . . . . 10 class ( x p y )
11		vs	. . . . . . . . . . 11 setvar s
12	11	cv 1363	. . . . . . . . . 10 class s
13	10, 12	wcel 2167	. . . . . . . . 9 wff ( x p y ) e. s
14	7, 5, 9	co 5922	. . . . . . . . . 10 class ( y p x )
15	14, 12	wcel 2167	. . . . . . . . 9 wff ( y p x ) e. s
16	13, 15	wb 105	. . . . . . . 8 wff ( ( x p y ) e. s <-> ( y p x ) e. s )
17		vb	. . . . . . . . 9 setvar b
18	17	cv 1363	. . . . . . . 8 class b
19	16, 6, 18	wral 2475	. . . . . . 7 wff A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s )
20	19, 4, 18	wral 2475	. . . . . 6 wff A. x e. b A. y e. b ( ( x p y ) e. s <-> ( y p x ) e. s )
21	2	cv 1363	. . . . . . 7 class w
22		cplusg 12755	. . . . . . 7 class +g
23	21, 22	cfv 5258	. . . . . 6 class ( +g ` w )
24	20, 8, 23	wsbc 2989	. . . . 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 12678	. . . . . 6 class Base
26	21, 25	cfv 5258	. . . . 5 class ( Base ` w )
27	24, 17, 26	wsbc 2989	. . . 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 13297	. . . . 5 class SubGrp
29	21, 28	cfv 5258	. . . 4 class (SubGrp ` w )
30	27, 11, 29	crab 2479	. . 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 ) }
31	2, 3, 30	cmpt 4094	. 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 ) } )
32	1, 31	wceq 1364	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 ) } )

This definition is referenced by:  isnsg  13332