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

Definition df-nsg 14947
 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 SubGrp
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-nsg
StepHypRef Expression
1 cnsg 14944 . 2 NrmSGrp
2 vw . . 3
3 cgrp 14690 . . 3
4 vx . . . . . . . . . . . 12
54cv 1652 . . . . . . . . . . 11
6 vy . . . . . . . . . . . 12
76cv 1652 . . . . . . . . . . 11
8 vp . . . . . . . . . . . 12
98cv 1652 . . . . . . . . . . 11
105, 7, 9co 6084 . . . . . . . . . 10
11 vs . . . . . . . . . . 11
1211cv 1652 . . . . . . . . . 10
1310, 12wcel 1726 . . . . . . . . 9
147, 5, 9co 6084 . . . . . . . . . 10
1514, 12wcel 1726 . . . . . . . . 9
1613, 15wb 178 . . . . . . . 8
17 vb . . . . . . . . 9
1817cv 1652 . . . . . . . 8
1916, 6, 18wral 2707 . . . . . . 7
2019, 4, 18wral 2707 . . . . . 6
212cv 1652 . . . . . . 7
22 cplusg 13534 . . . . . . 7
2321, 22cfv 5457 . . . . . 6
2420, 8, 23wsbc 3163 . . . . 5
25 cbs 13474 . . . . . 6
2621, 25cfv 5457 . . . . 5
2724, 17, 26wsbc 3163 . . . 4
28 csubg 14943 . . . . 5 SubGrp
2921, 28cfv 5457 . . . 4 SubGrp
3027, 11, 29crab 2711 . . 3 SubGrp
312, 3, 30cmpt 4269 . 2 SubGrp
321, 31wceq 1653 1 NrmSGrp SubGrp
 Colors of variables: wff set class This definition is referenced by:  isnsg  14974
 Copyright terms: Public domain W3C validator