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 = w ∈ Grp ⟼ s ∈ SubGrp ⁡ w | [˙Base w / b]˙ [˙+ w / p]˙ ∀ x ∈ b ∀ y ∈ b x p y ∈ s ↔ y p x ∈ s

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnsg class NrmSGrp
1 vw setvar w
2 cgrp class Grp
3 vs setvar s
4 csubg class SubGrp
5 1 cv setvar w
6 5 4 cfv class SubGrp ⁡ w
7 cbs class Base
8 5 7 cfv class Base w
9 vb setvar b
10 cplusg class + 𝑔
11 5 10 cfv class + w
12 vp setvar p
13 vx setvar x
14 9 cv setvar b
15 vy setvar y
16 13 cv setvar x
17 12 cv setvar p
18 15 cv setvar y
19 16 18 17 co class x p y
20 3 cv setvar s
21 19 20 wcel wff x p y ∈ s
22 18 16 17 co class y p x
23 22 20 wcel wff y p x ∈ s
24 21 23 wb wff x p y ∈ s ↔ y p x ∈ s
25 24 15 14 wral wff ∀ y ∈ b x p y ∈ s ↔ y p x ∈ s
26 25 13 14 wral wff ∀ x ∈ b ∀ y ∈ b x p y ∈ s ↔ y p x ∈ s
27 26 12 11 wsbc wff [˙+ w / p]˙ ∀ x ∈ b ∀ y ∈ b x p y ∈ s ↔ y p x ∈ s
28 27 9 8 wsbc wff [˙Base w / b]˙ [˙+ w / p]˙ ∀ x ∈ b ∀ y ∈ b x p y ∈ s ↔ y p x ∈ s
29 28 3 6 crab class s ∈ SubGrp ⁡ w | [˙Base w / b]˙ [˙+ w / p]˙ ∀ x ∈ b ∀ y ∈ b x p y ∈ s ↔ y p x ∈ s
30 1 2 29 cmpt class w ∈ Grp ⟼ s ∈ SubGrp ⁡ w | [˙Base w / b]˙ [˙+ w / p]˙ ∀ x ∈ b ∀ y ∈ b x p y ∈ s ↔ y p x ∈ s
31 0 30 wceq wff NrmSGrp = w ∈ Grp ⟼ s ∈ SubGrp ⁡ w | [˙Base w / b]˙ [˙+ w / p]˙ ∀ x ∈ b ∀ y ∈ b x p y ∈ s ↔ y p x ∈ s