Definition df-mulg 13672

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 13671	. 2 class .g
2		vg	. . 3 setvar g
3		cvv 2799	. . 3 class _V
4		vn	. . . 4 setvar n
5		vx	. . . 4 setvar x
6		cz 9457	. . . 4 class ZZ
7	2	cv 1394	. . . . 5 class g
8		cbs 13047	. . . . 5 class Base
9	7, 8	cfv 5318	. . . 4 class ( Base ` g )
10	4	cv 1394	. . . . . 6 class n
11		cc0 8010	. . . . . 6 class 0
12	10, 11	wceq 1395	. . . . 5 wff n = 0
13		c0g 13304	. . . . . 6 class 0g
14	7, 13	cfv 5318	. . . . 5 class ( 0g ` g )
15		vs	. . . . . 6 setvar s
16		cplusg 13125	. . . . . . . 8 class +g
17	7, 16	cfv 5318	. . . . . . 7 class ( +g ` g )
18		cn 9121	. . . . . . . 8 class NN
19	5	cv 1394	. . . . . . . . 9 class x
20	19	csn 3666	. . . . . . . 8 class { x }
21	18, 20	cxp 4717	. . . . . . 7 class ( NN X. { x } )
22		c1 8011	. . . . . . 7 class 1
23	17, 21, 22	cseq 10681	. . . . . 6 class seq 1 ( ( +g ` g ) , ( NN X. { x } ) )
24		clt 8192	. . . . . . . 8 class <
25	11, 10, 24	wbr 4083	. . . . . . 7 wff 0 < n
26	15	cv 1394	. . . . . . . 8 class s
27	10, 26	cfv 5318	. . . . . . 7 class ( s ` n )
28	10	cneg 8329	. . . . . . . . 9 class -u n
29	28, 26	cfv 5318	. . . . . . . 8 class ( s ` -u n )
30		cminusg 13549	. . . . . . . . 9 class invg
31	7, 30	cfv 5318	. . . . . . . 8 class ( invg ` g )
32	29, 31	cfv 5318	. . . . . . 7 class ( ( invg ` g ) ` ( s ` -u n ) )
33	25, 27, 32	cif 3602	. . . . . 6 class if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) )
34	15, 23, 33	csb 3124	. . . . 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 3602	. . . 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 6009	. . 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 4145	. 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 1395	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  13673