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} = (r \in V, i \in V ⟼ \{⟨x, y⟩ \| (\{x, y\} \subseteq {Base}_{r} \land {inv}_{g} (r) (x) +_{r} y \in i)\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cqg	$class ~_{QG}$
1		vr	$setvar r$
2		cvv	$class V$
3		vi	$setvar i$
4		vx	$setvar x$
5		vy	$setvar y$
6	4	cv	$setvar x$
7	5	cv	$setvar y$
8	6 7	cpr	$class \{x, y\}$
9		cbs	$class Base$
10	1	cv	$setvar r$
11	10 9	cfv	$class {Base}_{r}$
12	8 11	wss	$wff \{x, y\} \subseteq {Base}_{r}$
13		cminusg	$class {inv}_{g}$
14	10 13	cfv	$class {inv}_{g} (r)$
15	6 14	cfv	$class {inv}_{g} (r) (x)$
16		cplusg	$class +_{𝑔}$
17	10 16	cfv	$class +_{r}$
18	15 7 17	co	$class ({inv}_{g} (r) (x) +_{r} y)$
19	3	cv	$setvar i$
20	18 19	wcel	$wff {inv}_{g} (r) (x) +_{r} y \in i$
21	12 20	wa	$wff (\{x, y\} \subseteq {Base}_{r} \land {inv}_{g} (r) (x) +_{r} y \in i)$
22	21 4 5	copab	$class \{⟨x, y⟩ \| (\{x, y\} \subseteq {Base}_{r} \land {inv}_{g} (r) (x) +_{r} y \in i)\}$
23	1 3 2 2 22	cmpo	$class (r \in V, i \in V ⟼ \{⟨x, y⟩ \| (\{x, y\} \subseteq {Base}_{r} \land {inv}_{g} (r) (x) +_{r} y \in i)\})$
24	0 23	wceq	$wff ~_{QG} = (r \in V, i \in V ⟼ \{⟨x, y⟩ \| (\{x, y\} \subseteq {Base}_{r} \land {inv}_{g} (r) (x) +_{r} y \in i)\})$

Metamath Proof Explorer

Definition df-eqg

Detailed syntax breakdown