Definition df-nsg

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)

	Ref	Expression
Assertion	df-nsg	$$⊢\mathrm{NrmSGrp}=\left(w\in \mathrm{Grp}⟼\left\{s\in \mathrm{SubGrp}\left(w\right)|\underset{\dot{}}{[}{\mathrm{Base}}_w/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_w/p\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xpy\in s\leftrightarrow ypx\in s\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnsg	$$class\mathrm{NrmSGrp}$$
1		vw	$$setvarw$$
2		cgrp	$$class\mathrm{Grp}$$
3		vs	$$setvars$$
4		csubg	$$class\mathrm{SubGrp}$$
5	1	cv	$$setvarw$$
6	5 4	cfv	$$class\mathrm{SubGrp}\left(w\right)$$
7		cbs	$$class\mathrm{Base}$$
8	5 7	cfv	$$class{\mathrm{Base}}_w$$
9		vb	$$setvarb$$
10		cplusg	$$class{+}_{𝑔}$$
11	5 10	cfv	$$class{+}_w$$
12		vp	$$setvarp$$
13		vx	$$setvarx$$
14	9	cv	$$setvarb$$
15		vy	$$setvary$$
16	13	cv	$$setvarx$$
17	12	cv	$$setvarp$$
18	15	cv	$$setvary$$
19	16 18 17	co	$$class\left(xpy\right)$$
20	3	cv	$$setvars$$
21	19 20	wcel	$$wffxpy\in s$$
22	18 16 17	co	$$class\left(ypx\right)$$
23	22 20	wcel	$$wffypx\in s$$
24	21 23	wb	$$wff\left(xpy\in s\leftrightarrow ypx\in s\right)$$
25	24 15 14	wral	$$wff\forall y\in b\left(xpy\in s\leftrightarrow ypx\in s\right)$$
26	25 13 14	wral	$$wff\forall x\in b\forall y\in b\left(xpy\in s\leftrightarrow ypx\in s\right)$$
27	26 12 11	wsbc	$$wff\underset{\dot{}}{[}{+}_w/p\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xpy\in s\leftrightarrow ypx\in s\right)$$
28	27 9 8	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_w/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_w/p\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xpy\in s\leftrightarrow ypx\in s\right)$$
29	28 3 6	crab	$$class\left\{s\in \mathrm{SubGrp}\left(w\right)|\underset{\dot{}}{[}{\mathrm{Base}}_w/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_w/p\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xpy\in s\leftrightarrow ypx\in s\right)\right\}$$
30	1 2 29	cmpt	$$class\left(w\in \mathrm{Grp}⟼\left\{s\in \mathrm{SubGrp}\left(w\right)|\underset{\dot{}}{[}{\mathrm{Base}}_w/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_w/p\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xpy\in s\leftrightarrow ypx\in s\right)\right\}\right)$$
31	0 30	wceq	$$wff\mathrm{NrmSGrp}=\left(w\in \mathrm{Grp}⟼\left\{s\in \mathrm{SubGrp}\left(w\right)|\underset{\dot{}}{[}{\mathrm{Base}}_w/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_w/p\underset{\dot{}}{]}\forall x\in b\forall y\in b\left(xpy\in s\leftrightarrow ypx\in s\right)\right\}\right)$$