Definition df-ginv

Description: Define a function that maps a group operation to the group's inverse function. (Contributed by NM, 26-Oct-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ginv	|- inv = ( g e. GrpOp |-> ( x e. ran g |-> ( iota_ z e. ran g ( z g x ) = ( GId ` g ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgn	|- inv
1		vg	|- g
2		cgr	|- GrpOp
3		vx	|- x
4	1	cv	|- g
5	4	crn	|- ran g
6		vz	|- z
7	6	cv	|- z
8	3	cv	|- x
9	7 8 4	co	|- ( z g x )
10		cgi	|- GId
11	4 10	cfv	|- ( GId ` g )
12	9 11	wceq	|- ( z g x ) = ( GId ` g )
13	12 6 5	crio	|- ( iota_ z e. ran g ( z g x ) = ( GId ` g ) )
14	3 5 13	cmpt	|- ( x e. ran g |-> ( iota_ z e. ran g ( z g x ) = ( GId ` g ) ) )
15	1 2 14	cmpt	|- ( g e. GrpOp |-> ( x e. ran g |-> ( iota_ z e. ran g ( z g x ) = ( GId ` g ) ) ) )
16	0 15	wceq	|- inv = ( g e. GrpOp |-> ( x e. ran g |-> ( iota_ z e. ran g ( z g x ) = ( GId ` g ) ) ) )