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 e. GrpOp |-> ( x e. ran g , y e. ran g |-> ( x g ( ( inv ` g ) ` y ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgs	|- /g
1		vg	|- g
2		cgr	|- GrpOp
3		vx	|- x
4	1	cv	|- g
5	4	crn	|- ran g
6		vy	|- y
7	3	cv	|- x
8		cgn	|- inv
9	4 8	cfv	|- ( inv ` g )
10	6	cv	|- y
11	10 9	cfv	|- ( ( inv ` g ) ` y )
12	7 11 4	co	|- ( x g ( ( inv ` g ) ` y ) )
13	3 6 5 5 12	cmpo	|- ( x e. ran g , y e. ran g |-> ( x g ( ( inv ` g ) ` y ) ) )
14	1 2 13	cmpt	|- ( g e. GrpOp |-> ( x e. ran g , y e. ran g |-> ( x g ( ( inv ` g ) ` y ) ) ) )
15	0 14	wceq	|- /g = ( g e. GrpOp |-> ( x e. ran g , y e. ran g |-> ( x g ( ( inv ` g ) ` y ) ) ) )