MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nsg Structured version   Visualization version   GIF version

Definition df-nsg 17524
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
StepHypRef Expression
1 cnsg 17521 . 2 class NrmSGrp
2 vw . . 3 setvar 𝑤
3 cgrp 17354 . . 3 class Grp
4 vx . . . . . . . . . . . 12 setvar 𝑥
54cv 1479 . . . . . . . . . . 11 class 𝑥
6 vy . . . . . . . . . . . 12 setvar 𝑦
76cv 1479 . . . . . . . . . . 11 class 𝑦
8 vp . . . . . . . . . . . 12 setvar 𝑝
98cv 1479 . . . . . . . . . . 11 class 𝑝
105, 7, 9co 6610 . . . . . . . . . 10 class (𝑥𝑝𝑦)
11 vs . . . . . . . . . . 11 setvar 𝑠
1211cv 1479 . . . . . . . . . 10 class 𝑠
1310, 12wcel 1987 . . . . . . . . 9 wff (𝑥𝑝𝑦) ∈ 𝑠
147, 5, 9co 6610 . . . . . . . . . 10 class (𝑦𝑝𝑥)
1514, 12wcel 1987 . . . . . . . . 9 wff (𝑦𝑝𝑥) ∈ 𝑠
1613, 15wb 196 . . . . . . . 8 wff ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
17 vb . . . . . . . . 9 setvar 𝑏
1817cv 1479 . . . . . . . 8 class 𝑏
1916, 6, 18wral 2907 . . . . . . 7 wff 𝑦𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
2019, 4, 18wral 2907 . . . . . 6 wff 𝑥𝑏𝑦𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
212cv 1479 . . . . . . 7 class 𝑤
22 cplusg 15873 . . . . . . 7 class +g
2321, 22cfv 5852 . . . . . 6 class (+g𝑤)
2420, 8, 23wsbc 3421 . . . . 5 wff [(+g𝑤) / 𝑝]𝑥𝑏𝑦𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
25 cbs 15792 . . . . . 6 class Base
2621, 25cfv 5852 . . . . 5 class (Base‘𝑤)
2724, 17, 26wsbc 3421 . . . 4 wff [(Base‘𝑤) / 𝑏][(+g𝑤) / 𝑝]𝑥𝑏𝑦𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)
28 csubg 17520 . . . . 5 class SubGrp
2921, 28cfv 5852 . . . 4 class (SubGrp‘𝑤)
3027, 11, 29crab 2911 . . 3 class {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g𝑤) / 𝑝]𝑥𝑏𝑦𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)}
312, 3, 30cmpt 4678 . 2 class (𝑤 ∈ Grp ↦ {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g𝑤) / 𝑝]𝑥𝑏𝑦𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)})
321, 31wceq 1480 1 wff NrmSGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g𝑤) / 𝑝]𝑥𝑏𝑦𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)})
Colors of variables: wff setvar class
This definition is referenced by:  isnsg  17555
  Copyright terms: Public domain W3C validator