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 = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑟 ) ∧ ( ( ( invg𝑟 ) ‘ 𝑥 ) ( +g𝑟 ) 𝑦 ) ∈ 𝑖 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cqg ~QG
1 vr 𝑟
2 cvv V
3 vi 𝑖
4 vx 𝑥
5 vy 𝑦
6 4 cv 𝑥
7 5 cv 𝑦
8 6 7 cpr { 𝑥 , 𝑦 }
9 cbs Base
10 1 cv 𝑟
11 10 9 cfv ( Base ‘ 𝑟 )
12 8 11 wss { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑟 )
13 cminusg invg
14 10 13 cfv ( invg𝑟 )
15 6 14 cfv ( ( invg𝑟 ) ‘ 𝑥 )
16 cplusg +g
17 10 16 cfv ( +g𝑟 )
18 15 7 17 co ( ( ( invg𝑟 ) ‘ 𝑥 ) ( +g𝑟 ) 𝑦 )
19 3 cv 𝑖
20 18 19 wcel ( ( ( invg𝑟 ) ‘ 𝑥 ) ( +g𝑟 ) 𝑦 ) ∈ 𝑖
21 12 20 wa ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑟 ) ∧ ( ( ( invg𝑟 ) ‘ 𝑥 ) ( +g𝑟 ) 𝑦 ) ∈ 𝑖 )
22 21 4 5 copab { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑟 ) ∧ ( ( ( invg𝑟 ) ‘ 𝑥 ) ( +g𝑟 ) 𝑦 ) ∈ 𝑖 ) }
23 1 3 2 2 22 cmpo ( 𝑟 ∈ V , 𝑖 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑟 ) ∧ ( ( ( invg𝑟 ) ‘ 𝑥 ) ( +g𝑟 ) 𝑦 ) ∈ 𝑖 ) } )
24 0 23 wceq ~QG = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑟 ) ∧ ( ( ( invg𝑟 ) ‘ 𝑥 ) ( +g𝑟 ) 𝑦 ) ∈ 𝑖 ) } )