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	⊢ NrmSGrp = ( 𝑤 ∈ Grp ↦ { 𝑠 ∈ ( SubGrp ‘ 𝑤 ) ∣ [ ( Base ‘ 𝑤 ) / 𝑏 ] [ ( +g ‘ 𝑤 ) / 𝑝 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnsg	⊢ NrmSGrp
1		vw	⊢ 𝑤
2		cgrp	⊢ Grp
3		vs	⊢ 𝑠
4		csubg	⊢ SubGrp
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( SubGrp ‘ 𝑤 )
7		cbs	⊢ Base
8	5 7	cfv	⊢ ( Base ‘ 𝑤 )
9		vb	⊢ 𝑏
10		cplusg	⊢ +g
11	5 10	cfv	⊢ ( +g ‘ 𝑤 )
12		vp	⊢ 𝑝
13		vx	⊢ 𝑥
14	9	cv	⊢ 𝑏
15		vy	⊢ 𝑦
16	13	cv	⊢ 𝑥
17	12	cv	⊢ 𝑝
18	15	cv	⊢ 𝑦
19	16 18 17	co	⊢ ( 𝑥 𝑝 𝑦 )
20	3	cv	⊢ 𝑠
21	19 20	wcel	⊢ ( 𝑥 𝑝 𝑦 ) ∈ 𝑠
22	18 16 17	co	⊢ ( 𝑦 𝑝 𝑥 )
23	22 20	wcel	⊢ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠
24	21 23	wb	⊢ ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 )
25	24 15 14	wral	⊢ ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 )
26	25 13 14	wral	⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 )
27	26 12 11	wsbc	⊢ [ ( +g ‘ 𝑤 ) / 𝑝 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 )
28	27 9 8	wsbc	⊢ [ ( Base ‘ 𝑤 ) / 𝑏 ] [ ( +g ‘ 𝑤 ) / 𝑝 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 )
29	28 3 6	crab	⊢ { 𝑠 ∈ ( SubGrp ‘ 𝑤 ) ∣ [ ( Base ‘ 𝑤 ) / 𝑏 ] [ ( +g ‘ 𝑤 ) / 𝑝 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) }
30	1 2 29	cmpt	⊢ ( 𝑤 ∈ Grp ↦ { 𝑠 ∈ ( SubGrp ‘ 𝑤 ) ∣ [ ( Base ‘ 𝑤 ) / 𝑏 ] [ ( +g ‘ 𝑤 ) / 𝑝 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) } )
31	0 30	wceq	⊢ NrmSGrp = ( 𝑤 ∈ Grp ↦ { 𝑠 ∈ ( SubGrp ‘ 𝑤 ) ∣ [ ( Base ‘ 𝑤 ) / 𝑏 ] [ ( +g ‘ 𝑤 ) / 𝑝 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) } )