Definition df-eqg 19000

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

Step	Hyp	Ref	Expression
1		cqg 18997	. 2 class ~QG
2		vr	. . 3 setvar 𝑟
3		vi	. . 3 setvar 𝑖
4		cvv 3475	. . 3 class V
5		vx	. . . . . . . 8 setvar 𝑥
6	5	cv 1541	. . . . . . 7 class 𝑥
7		vy	. . . . . . . 8 setvar 𝑦
8	7	cv 1541	. . . . . . 7 class 𝑦
9	6, 8	cpr 4630	. . . . . 6 class {𝑥, 𝑦}
10	2	cv 1541	. . . . . . 7 class 𝑟
11		cbs 17141	. . . . . . 7 class Base
12	10, 11	cfv 6541	. . . . . 6 class (Base‘𝑟)
13	9, 12	wss 3948	. . . . 5 wff {𝑥, 𝑦} ⊆ (Base‘𝑟)
14		cminusg 18817	. . . . . . . . 9 class invg
15	10, 14	cfv 6541	. . . . . . . 8 class (invg‘𝑟)
16	6, 15	cfv 6541	. . . . . . 7 class ((invg‘𝑟)‘𝑥)
17		cplusg 17194	. . . . . . . 8 class +g
18	10, 17	cfv 6541	. . . . . . 7 class (+g‘𝑟)
19	16, 8, 18	co 7406	. . . . . 6 class (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦)
20	3	cv 1541	. . . . . 6 class 𝑖
21	19, 20	wcel 2107	. . . . 5 wff (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖
22	13, 21	wa 397	. . . 4 wff ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖)
23	22, 5, 7	copab 5210	. . 3 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖)}
24	2, 3, 4, 4, 23	cmpo 7408	. 2 class (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖)})
25	1, 24	wceq 1542	1 wff ~QG = (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖)})

This definition is referenced by:  releqg  19050  eqgfval  19051