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