Definition df-mulg

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

	Ref	Expression
Assertion	df-mulg	$$⊢{\mathrm{\cdot }}_{𝑔}=\left(g\in \mathrm{V}⟼\left(n\in \mathbb{Z},x\in {\mathrm{Base}}_g⟼if\left(n=0,0_g,⦋seq1\left({+}_g,\left(\mathbb{N}\times \left\{x\right\}\right)\right)/s⦌if\left(0<n,s\left(n\right),{inv}_g\left(g\right)\left(s\left(-n\right)\right)\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmg	$$class{\mathrm{\cdot }}_{𝑔}$$
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		vn	$$setvarn$$
4		cz	$$class\mathbb{Z}$$
5		vx	$$setvarx$$
6		cbs	$$class\mathrm{Base}$$
7	1	cv	$$setvarg$$
8	7 6	cfv	$$class{\mathrm{Base}}_g$$
9	3	cv	$$setvarn$$
10		cc0	$$class0$$
11	9 10	wceq	$$wffn=0$$
12		c0g	$$class{0}_{𝑔}$$
13	7 12	cfv	$$class{0}_g$$
14		c1	$$class1$$
15		cplusg	$$class{+}_{𝑔}$$
16	7 15	cfv	$$class{+}_g$$
17		cn	$$class\mathbb{N}$$
18	5	cv	$$setvarx$$
19	18	csn	$$class\left\{x\right\}$$
20	17 19	cxp	$$class\left(\mathbb{N}\times \left\{x\right\}\right)$$
21	16 20 14	cseq	$$classseq1\left({+}_g,\left(\mathbb{N}\times \left\{x\right\}\right)\right)$$
22		vs	$$setvars$$
23		clt	$$class<$$
24	10 9 23	wbr	$$wff0<n$$
25	22	cv	$$setvars$$
26	9 25	cfv	$$classs\left(n\right)$$
27		cminusg	$$class{inv}_g$$
28	7 27	cfv	$$class{inv}_g\left(g\right)$$
29	9	cneg	$$class\left(-n\right)$$
30	29 25	cfv	$$classs\left(-n\right)$$
31	30 28	cfv	$$class{inv}_g\left(g\right)\left(s\left(-n\right)\right)$$
32	24 26 31	cif	$$classif\left(0<n,s\left(n\right),{inv}_g\left(g\right)\left(s\left(-n\right)\right)\right)$$
33	22 21 32	csb	$$class⦋seq1\left({+}_g,\left(\mathbb{N}\times \left\{x\right\}\right)\right)/s⦌if\left(0<n,s\left(n\right),{inv}_g\left(g\right)\left(s\left(-n\right)\right)\right)$$
34	11 13 33	cif	$$classif\left(n=0,0_g,⦋seq1\left({+}_g,\left(\mathbb{N}\times \left\{x\right\}\right)\right)/s⦌if\left(0<n,s\left(n\right),{inv}_g\left(g\right)\left(s\left(-n\right)\right)\right)\right)$$
35	3 5 4 8 34	cmpo	$$class\left(n\in \mathbb{Z},x\in {\mathrm{Base}}_g⟼if\left(n=0,0_g,⦋seq1\left({+}_g,\left(\mathbb{N}\times \left\{x\right\}\right)\right)/s⦌if\left(0<n,s\left(n\right),{inv}_g\left(g\right)\left(s\left(-n\right)\right)\right)\right)\right)$$
36	1 2 35	cmpt	$$class\left(g\in \mathrm{V}⟼\left(n\in \mathbb{Z},x\in {\mathrm{Base}}_g⟼if\left(n=0,0_g,⦋seq1\left({+}_g,\left(\mathbb{N}\times \left\{x\right\}\right)\right)/s⦌if\left(0<n,s\left(n\right),{inv}_g\left(g\right)\left(s\left(-n\right)\right)\right)\right)\right)\right)$$
37	0 36	wceq	$$wff{\mathrm{\cdot }}_{𝑔}=\left(g\in \mathrm{V}⟼\left(n\in \mathbb{Z},x\in {\mathrm{Base}}_g⟼if\left(n=0,0_g,⦋seq1\left({+}_g,\left(\mathbb{N}\times \left\{x\right\}\right)\right)/s⦌if\left(0<n,s\left(n\right),{inv}_g\left(g\right)\left(s\left(-n\right)\right)\right)\right)\right)\right)$$