Definition df-nsg 18668

Description: Define the equivalence relation in a quotient ring or quotient group (where 𝑖 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 = (𝑤 ∈ Grp ↦ {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)})

Distinct variable group:   𝑝,𝑏,𝑠,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-nsg

Step	Hyp	Ref	Expression
1		cnsg 18665	. 2 class NrmSGrp
2		vw	. . 3 setvar 𝑤
3		cgrp 18492	. . 3 class Grp
4		vx	. . . . . . . . . . . 12 setvar 𝑥
5	4	cv 1538	. . . . . . . . . . 11 class 𝑥
6		vy	. . . . . . . . . . . 12 setvar 𝑦
7	6	cv 1538	. . . . . . . . . . 11 class 𝑦
8		vp	. . . . . . . . . . . 12 setvar 𝑝
9	8	cv 1538	. . . . . . . . . . 11 class 𝑝
10	5, 7, 9	co 7255	. . . . . . . . . 10 class (𝑥𝑝𝑦)
11		vs	. . . . . . . . . . 11 setvar 𝑠
12	11	cv 1538	. . . . . . . . . 10 class 𝑠
13	10, 12	wcel 2108	. . . . . . . . 9 wff (𝑥𝑝𝑦) ∈ 𝑠
14	7, 5, 9	co 7255	. . . . . . . . . 10 class (𝑦𝑝𝑥)
15	14, 12	wcel 2108	. . . . . . . . 9 wff (𝑦𝑝𝑥) ∈ 𝑠
16	13, 15	wb 205	. . . . . . . 8 wff ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
17		vb	. . . . . . . . 9 setvar 𝑏
18	17	cv 1538	. . . . . . . 8 class 𝑏
19	16, 6, 18	wral 3063	. . . . . . 7 wff ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
20	19, 4, 18	wral 3063	. . . . . 6 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
21	2	cv 1538	. . . . . . 7 class 𝑤
22		cplusg 16888	. . . . . . 7 class +g
23	21, 22	cfv 6418	. . . . . 6 class (+g‘𝑤)
24	20, 8, 23	wsbc 3711	. . . . 5 wff [(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
25		cbs 16840	. . . . . 6 class Base
26	21, 25	cfv 6418	. . . . 5 class (Base‘𝑤)
27	24, 17, 26	wsbc 3711	. . . 4 wff [(Base‘𝑤) / 𝑏][(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
28		csubg 18664	. . . . 5 class SubGrp
29	21, 28	cfv 6418	. . . 4 class (SubGrp‘𝑤)
30	27, 11, 29	crab 3067	. . 3 class {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)}
31	2, 3, 30	cmpt 5153	. 2 class (𝑤 ∈ Grp ↦ {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)})
32	1, 31	wceq 1539	1 wff NrmSGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)})

This definition is referenced by:  isnsg  18698