Definition df-mulg 13837

Description: Define the group multiple function, also known as group exponentiation when viewed multiplicatively. (Contributed by Mario Carneiro, 11-Dec-2014.)

Assertion

Ref	Expression
df-mulg	|- .g = ( g e. _V |-> ( n e. ZZ , x e. ( Base ` g ) |-> if ( n = 0 , ( 0g ` g ) , [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) ) ) ) )

Distinct variable group:   g, n, s, x

Detailed syntax breakdown of Definition df-mulg

Step	Hyp	Ref	Expression
1		cmg 13836	. 2 class .g
2		vg	. . 3 setvar g
3		cvv 2813	. . 3 class _V
4		vn	. . . 4 setvar n
5		vx	. . . 4 setvar x
6		cz 9577	. . . 4 class ZZ
7	2	cv 1397	. . . . 5 class g
8		cbs 13212	. . . . 5 class Base
9	7, 8	cfv 5352	. . . 4 class ( Base ` g )
10	4	cv 1397	. . . . . 6 class n
11		cc0 8127	. . . . . 6 class 0
12	10, 11	wceq 1398	. . . . 5 wff n = 0
13		c0g 13469	. . . . . 6 class 0g
14	7, 13	cfv 5352	. . . . 5 class ( 0g ` g )
15		vs	. . . . . 6 setvar s
16		cplusg 13290	. . . . . . . 8 class +g
17	7, 16	cfv 5352	. . . . . . 7 class ( +g ` g )
18		cn 9237	. . . . . . . 8 class NN
19	5	cv 1397	. . . . . . . . 9 class x
20	19	csn 3689	. . . . . . . 8 class { x }
21	18, 20	cxp 4747	. . . . . . 7 class ( NN X. { x } )
22		c1 8128	. . . . . . 7 class 1
23	17, 21, 22	cseq 10809	. . . . . 6 class seq 1 ( ( +g ` g ) , ( NN X. { x } ) )
24		clt 8308	. . . . . . . 8 class <
25	11, 10, 24	wbr 4109	. . . . . . 7 wff 0 < n
26	15	cv 1397	. . . . . . . 8 class s
27	10, 26	cfv 5352	. . . . . . 7 class ( s ` n )
28	10	cneg 8445	. . . . . . . . 9 class -u n
29	28, 26	cfv 5352	. . . . . . . 8 class ( s ` -u n )
30		cminusg 13714	. . . . . . . . 9 class invg
31	7, 30	cfv 5352	. . . . . . . 8 class ( invg ` g )
32	29, 31	cfv 5352	. . . . . . 7 class ( ( invg ` g ) ` ( s ` -u n ) )
33	25, 27, 32	cif 3620	. . . . . 6 class if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) )
34	15, 23, 33	csb 3138	. . . . 5 class [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) )
35	12, 14, 34	cif 3620	. . . 4 class if ( n = 0 , ( 0g ` g ) , [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) ) )
36	4, 5, 6, 9, 35	cmpo 6052	. . 3 class ( n e. ZZ , x e. ( Base ` g ) |-> if ( n = 0 , ( 0g ` g ) , [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) ) ) )
37	2, 3, 36	cmpt 4171	. 2 class ( g e. _V |-> ( n e. ZZ , x e. ( Base ` g ) |-> if ( n = 0 , ( 0g ` g ) , [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) ) ) ) )
38	1, 37	wceq 1398	1 wff .g = ( g e. _V |-> ( n e. ZZ , x e. ( Base ` g ) |-> if ( n = 0 , ( 0g ` g ) , [_ seq 1 ( ( +g ` g ) , ( NN X. { x } ) ) / s ]_ if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) ) ) ) )

This definition is referenced by:  mulgfvalg  13838