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 = ( 𝑟 ∈ 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 ‘ 𝑟 ) 𝑦 ) ∈ 𝑖 ) } )