This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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