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

Metamath Proof Explorer

Definition df-eqg

Description: Define the equivalence relation in a group generated by a subgroup. More precisely, if G is a group and H is a subgroup, then G ~QG H is the equivalence relation on G associated with the left cosets of H . A typical application of this definition is the construction of the quotient group (resp. ring) of a group (resp. ring) by a normal subgroup (resp. two-sided ideal). (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Assertion df-eqg ⊢ ~ QG = r ∈ V , i ∈ V ⟼ x y | x y ⊆ Base r ∧ inv g ⁡ r ⁡ x + r y ∈ i

Detailed syntax breakdown

Step Hyp Ref Expression
0 cqg class ~ QG
1 vr setvar r
2 cvv class V
3 vi setvar i
4 vx setvar x
5 vy setvar y
6 4 cv setvar x
7 5 cv setvar y
8 6 7 cpr class x y
9 cbs class Base
10 1 cv setvar r
11 10 9 cfv class Base r
12 8 11 wss wff x y ⊆ Base r
13 cminusg class inv g
14 10 13 cfv class inv g ⁡ r
15 6 14 cfv class inv g ⁡ r ⁡ x
16 cplusg class + 𝑔
17 10 16 cfv class + r
18 15 7 17 co class inv g ⁡ r ⁡ x + r y
19 3 cv setvar i
20 18 19 wcel wff inv g ⁡ r ⁡ x + r y ∈ i
21 12 20 wa wff x y ⊆ Base r ∧ inv g ⁡ r ⁡ x + r y ∈ i
22 21 4 5 copab class x y | x y ⊆ Base r ∧ inv g ⁡ r ⁡ x + r y ∈ i
23 1 3 2 2 22 cmpo class r ∈ V , i ∈ V ⟼ x y | x y ⊆ Base r ∧ inv g ⁡ r ⁡ x + r y ∈ i
24 0 23 wceq wff ~ QG = r ∈ V , i ∈ V ⟼ x y | x y ⊆ Base r ∧ inv g ⁡ r ⁡ x + r y ∈ i