Definition df-nsg 13301

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 13298	. 2 class NrmSGrp
2		vw	. . 3 setvar 𝑤
3		cgrp 13132	. . 3 class Grp
4		vx	. . . . . . . . . . . 12 setvar 𝑥
5	4	cv 1363	. . . . . . . . . . 11 class 𝑥
6		vy	. . . . . . . . . . . 12 setvar 𝑦
7	6	cv 1363	. . . . . . . . . . 11 class 𝑦
8		vp	. . . . . . . . . . . 12 setvar 𝑝
9	8	cv 1363	. . . . . . . . . . 11 class 𝑝
10	5, 7, 9	co 5922	. . . . . . . . . 10 class (𝑥𝑝𝑦)
11		vs	. . . . . . . . . . 11 setvar 𝑠
12	11	cv 1363	. . . . . . . . . 10 class 𝑠
13	10, 12	wcel 2167	. . . . . . . . 9 wff (𝑥𝑝𝑦) ∈ 𝑠
14	7, 5, 9	co 5922	. . . . . . . . . 10 class (𝑦𝑝𝑥)
15	14, 12	wcel 2167	. . . . . . . . 9 wff (𝑦𝑝𝑥) ∈ 𝑠
16	13, 15	wb 105	. . . . . . . 8 wff ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
17		vb	. . . . . . . . 9 setvar 𝑏
18	17	cv 1363	. . . . . . . 8 class 𝑏
19	16, 6, 18	wral 2475	. . . . . . 7 wff ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
20	19, 4, 18	wral 2475	. . . . . 6 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
21	2	cv 1363	. . . . . . 7 class 𝑤
22		cplusg 12755	. . . . . . 7 class +g
23	21, 22	cfv 5258	. . . . . 6 class (+g‘𝑤)
24	20, 8, 23	wsbc 2989	. . . . 5 wff [(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
25		cbs 12678	. . . . . 6 class Base
26	21, 25	cfv 5258	. . . . 5 class (Base‘𝑤)
27	24, 17, 26	wsbc 2989	. . . 4 wff [(Base‘𝑤) / 𝑏][(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
28		csubg 13297	. . . . 5 class SubGrp
29	21, 28	cfv 5258	. . . 4 class (SubGrp‘𝑤)
30	27, 11, 29	crab 2479	. . 3 class {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)}
31	2, 3, 30	cmpt 4094	. 2 class (𝑤 ∈ Grp ↦ {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)})
32	1, 31	wceq 1364	1 wff NrmSGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)})

This definition is referenced by:  isnsg  13332