Metamath Proof Explorer


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𝑤 ) / 𝑝 ]𝑥𝑏𝑦𝑏 ( ( 𝑥 𝑝 𝑦 ) ∈ 𝑠 ↔ ( 𝑦 𝑝 𝑥 ) ∈ 𝑠 ) } )