Definition df-minusg 12835

Description: Define inverse of group element. (Contributed by NM, 24-Aug-2011.)

Assertion

Ref	Expression
df-minusg	|- invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )

Distinct variable group:   w, g, x

Detailed syntax breakdown of Definition df-minusg

Step	Hyp	Ref	Expression
1		cminusg 12832	. 2 class invg
2		vg	. . 3 setvar g
3		cvv 2737	. . 3 class _V
4		vx	. . . 4 setvar x
5	2	cv 1352	. . . . 5 class g
6		cbs 12456	. . . . 5 class Base
7	5, 6	cfv 5216	. . . 4 class ( Base ` g )
8		vw	. . . . . . . 8 setvar w
9	8	cv 1352	. . . . . . 7 class w
10	4	cv 1352	. . . . . . 7 class x
11		cplusg 12530	. . . . . . . 8 class +g
12	5, 11	cfv 5216	. . . . . . 7 class ( +g ` g )
13	9, 10, 12	co 5874	. . . . . 6 class ( w ( +g ` g ) x )
14		c0g 12695	. . . . . . 7 class 0g
15	5, 14	cfv 5216	. . . . . 6 class ( 0g ` g )
16	13, 15	wceq 1353	. . . . 5 wff ( w ( +g ` g ) x ) = ( 0g ` g )
17	16, 8, 7	crio 5829	. . . 4 class ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) )
18	4, 7, 17	cmpt 4064	. . 3 class ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) )
19	2, 3, 18	cmpt 4064	. 2 class ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )
20	1, 19	wceq 1353	1 wff invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ w e. ( Base ` g ) ( w ( +g ` g ) x ) = ( 0g ` g ) ) ) )

This definition is referenced by:  grpinvfvalg  12869