Definition df-mulg 17541

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 17540	. 2 class .g
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		vn	. . . 4 setvar n
5		vx	. . . 4 setvar x
6		cz 11377	. . . 4 class ZZ
7	2	cv 1482	. . . . 5 class g
8		cbs 15857	. . . . 5 class Base
9	7, 8	cfv 5888	. . . 4 class ( Base ` g )
10	4	cv 1482	. . . . . 6 class n
11		cc0 9936	. . . . . 6 class 0
12	10, 11	wceq 1483	. . . . 5 wff n = 0
13		c0g 16100	. . . . . 6 class 0g
14	7, 13	cfv 5888	. . . . 5 class ( 0g ` g )
15		vs	. . . . . 6 setvar s
16		cplusg 15941	. . . . . . . 8 class +g
17	7, 16	cfv 5888	. . . . . . 7 class ( +g ` g )
18		cn 11020	. . . . . . . 8 class NN
19	5	cv 1482	. . . . . . . . 9 class x
20	19	csn 4177	. . . . . . . 8 class { x }
21	18, 20	cxp 5112	. . . . . . 7 class ( NN X. { x } )
22		c1 9937	. . . . . . 7 class 1
23	17, 21, 22	cseq 12801	. . . . . 6 class seq 1 ( ( +g ` g ) , ( NN X. { x } ) )
24		clt 10074	. . . . . . . 8 class <
25	11, 10, 24	wbr 4653	. . . . . . 7 wff 0 < n
26	15	cv 1482	. . . . . . . 8 class s
27	10, 26	cfv 5888	. . . . . . 7 class ( s ` n )
28	10	cneg 10267	. . . . . . . . 9 class -u n
29	28, 26	cfv 5888	. . . . . . . 8 class ( s ` -u n )
30		cminusg 17423	. . . . . . . . 9 class invg
31	7, 30	cfv 5888	. . . . . . . 8 class ( invg ` g )
32	29, 31	cfv 5888	. . . . . . 7 class ( ( invg ` g ) ` ( s ` -u n ) )
33	25, 27, 32	cif 4086	. . . . . 6 class if ( 0 < n , ( s ` n ) , ( ( invg ` g ) ` ( s ` -u n ) ) )
34	15, 23, 33	csb 3533	. . . . 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 4086	. . . 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	cmpt2 6652	. . 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 4729	. 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 1483	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:  mulgfval  17542