Definition df-mulg 12840

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 12839	. 2 class .g
2		vg	. . 3 setvar g
3		cvv 2733	. . 3 class _V
4		vn	. . . 4 setvar n
5		vx	. . . 4 setvar x
6		cz 9221	. . . 4 class ZZ
7	2	cv 1350	. . . . 5 class g
8		cbs 12425	. . . . 5 class Base
9	7, 8	cfv 5205	. . . 4 class ( Base ` g )
10	4	cv 1350	. . . . . 6 class n
11		cc0 7783	. . . . . 6 class 0
12	10, 11	wceq 1351	. . . . 5 wff n = 0
13		c0g 12623	. . . . . 6 class 0g
14	7, 13	cfv 5205	. . . . 5 class ( 0g ` g )
15		vs	. . . . . 6 setvar s
16		cplusg 12489	. . . . . . . 8 class +g
17	7, 16	cfv 5205	. . . . . . 7 class ( +g ` g )
18		cn 8887	. . . . . . . 8 class NN
19	5	cv 1350	. . . . . . . . 9 class x
20	19	csn 3586	. . . . . . . 8 class { x }
21	18, 20	cxp 4615	. . . . . . 7 class ( NN X. { x } )
22		c1 7784	. . . . . . 7 class 1
23	17, 21, 22	cseq 10410	. . . . . 6 class seq 1 ( ( +g ` g ) , ( NN X. { x } ) )
24		clt 7963	. . . . . . . 8 class <
25	11, 10, 24	wbr 3995	. . . . . . 7 wff 0 < n
26	15	cv 1350	. . . . . . . 8 class s
27	10, 26	cfv 5205	. . . . . . 7 class ( s ` n )
28	10	cneg 8100	. . . . . . . . 9 class -u n
29	28, 26	cfv 5205	. . . . . . . 8 class ( s ` -u n )
30		cminusg 12736	. . . . . . . . 9 class invg
31	7, 30	cfv 5205	. . . . . . . 8 class ( invg ` g )
32	29, 31	cfv 5205	. . . . . . 7 class ( ( invg ` g ) ` ( s ` -u n ) )
33	25, 27, 32	cif 3529	. . . . . 6 class if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) )
34	15, 23, 33	csb 3052	. . . . 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 3529	. . . 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 5864	. . 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 4056	. 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 1351	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  12841