Definition df-mulg 13427

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 13426	. 2 class .g
2		vg	. . 3 setvar g
3		cvv 2771	. . 3 class _V
4		vn	. . . 4 setvar n
5		vx	. . . 4 setvar x
6		cz 9371	. . . 4 class ZZ
7	2	cv 1371	. . . . 5 class g
8		cbs 12803	. . . . 5 class Base
9	7, 8	cfv 5270	. . . 4 class ( Base ` g )
10	4	cv 1371	. . . . . 6 class n
11		cc0 7924	. . . . . 6 class 0
12	10, 11	wceq 1372	. . . . 5 wff n = 0
13		c0g 13059	. . . . . 6 class 0g
14	7, 13	cfv 5270	. . . . 5 class ( 0g ` g )
15		vs	. . . . . 6 setvar s
16		cplusg 12880	. . . . . . . 8 class +g
17	7, 16	cfv 5270	. . . . . . 7 class ( +g ` g )
18		cn 9035	. . . . . . . 8 class NN
19	5	cv 1371	. . . . . . . . 9 class x
20	19	csn 3632	. . . . . . . 8 class { x }
21	18, 20	cxp 4672	. . . . . . 7 class ( NN X. { x } )
22		c1 7925	. . . . . . 7 class 1
23	17, 21, 22	cseq 10590	. . . . . 6 class seq 1 ( ( +g ` g ) , ( NN X. { x } ) )
24		clt 8106	. . . . . . . 8 class <
25	11, 10, 24	wbr 4043	. . . . . . 7 wff 0 < n
26	15	cv 1371	. . . . . . . 8 class s
27	10, 26	cfv 5270	. . . . . . 7 class ( s ` n )
28	10	cneg 8243	. . . . . . . . 9 class -u n
29	28, 26	cfv 5270	. . . . . . . 8 class ( s ` -u n )
30		cminusg 13304	. . . . . . . . 9 class invg
31	7, 30	cfv 5270	. . . . . . . 8 class ( invg ` g )
32	29, 31	cfv 5270	. . . . . . 7 class ( ( invg ` g ) ` ( s ` -u n ) )
33	25, 27, 32	cif 3570	. . . . . 6 class if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) )
34	15, 23, 33	csb 3092	. . . . 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 3570	. . . 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 5945	. . 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 4104	. 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 1372	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  13428