Metamath Proof Explorer

Definition df-gdiv

Description: Define a function that maps a group operation to the group's division (or subtraction) operation. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-gdiv	$⊢ /_{g} = (g \in GrpOp ⟼ (x \in ran g, y \in ran g ⟼ x g inv (g) (y)))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgs	$class /_{g}$
1		vg	$setvar g$
2		cgr	$class GrpOp$
3		vx	$setvar x$
4	1	cv	$setvar g$
5	4	crn	$class ran g$
6		vy	$setvar y$
7	3	cv	$setvar x$
8		cgn	$class inv$
9	4 8	cfv	$class inv (g)$
10	6	cv	$setvar y$
11	10 9	cfv	$class inv (g) (y)$
12	7 11 4	co	$class (x g inv (g) (y))$
13	3 6 5 5 12	cmpo	$class (x \in ran g, y \in ran g ⟼ x g inv (g) (y))$
14	1 2 13	cmpt	$class (g \in GrpOp ⟼ (x \in ran g, y \in ran g ⟼ x g inv (g) (y)))$
15	0 14	wceq	$wff /_{g} = (g \in GrpOp ⟼ (x \in ran g, y \in ran g ⟼ x g inv (g) (y)))$