MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-eqg Structured version   Visualization version   GIF version

Definition df-eqg 17802
Description: Define the equivalence relation in a group generated by a subgroup. More precisely, if 𝐺 is a group and 𝐻 is a subgroup, then 𝐺 ~QG 𝐻 is the equivalence relation on 𝐺 associated with the left cosets of 𝐻. 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.)
Assertion
Ref Expression
df-eqg ~QG = (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg𝑟)‘𝑥)(+g𝑟)𝑦) ∈ 𝑖)})
Distinct variable group:   𝑖,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-eqg
StepHypRef Expression
1 cqg 17799 . 2 class ~QG
2 vr . . 3 setvar 𝑟
3 vi . . 3 setvar 𝑖
4 cvv 3402 . . 3 class V
5 vx . . . . . . . 8 setvar 𝑥
65cv 1636 . . . . . . 7 class 𝑥
7 vy . . . . . . . 8 setvar 𝑦
87cv 1636 . . . . . . 7 class 𝑦
96, 8cpr 4383 . . . . . 6 class {𝑥, 𝑦}
102cv 1636 . . . . . . 7 class 𝑟
11 cbs 16075 . . . . . . 7 class Base
1210, 11cfv 6108 . . . . . 6 class (Base‘𝑟)
139, 12wss 3780 . . . . 5 wff {𝑥, 𝑦} ⊆ (Base‘𝑟)
14 cminusg 17635 . . . . . . . . 9 class invg
1510, 14cfv 6108 . . . . . . . 8 class (invg𝑟)
166, 15cfv 6108 . . . . . . 7 class ((invg𝑟)‘𝑥)
17 cplusg 16160 . . . . . . . 8 class +g
1810, 17cfv 6108 . . . . . . 7 class (+g𝑟)
1916, 8, 18co 6881 . . . . . 6 class (((invg𝑟)‘𝑥)(+g𝑟)𝑦)
203cv 1636 . . . . . 6 class 𝑖
2119, 20wcel 2157 . . . . 5 wff (((invg𝑟)‘𝑥)(+g𝑟)𝑦) ∈ 𝑖
2213, 21wa 384 . . . 4 wff ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg𝑟)‘𝑥)(+g𝑟)𝑦) ∈ 𝑖)
2322, 5, 7copab 4917 . . 3 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg𝑟)‘𝑥)(+g𝑟)𝑦) ∈ 𝑖)}
242, 3, 4, 4, 23cmpt2 6883 . 2 class (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg𝑟)‘𝑥)(+g𝑟)𝑦) ∈ 𝑖)})
251, 24wceq 1637 1 wff ~QG = (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg𝑟)‘𝑥)(+g𝑟)𝑦) ∈ 𝑖)})
Colors of variables: wff setvar class
This definition is referenced by:  releqg  17850  eqgfval  17851
  Copyright terms: Public domain W3C validator