# Metamath Proof Explorer

## 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

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cmg ${class}{\cdot }_{𝑔}$
1 vg ${setvar}{g}$
2 cvv ${class}\mathrm{V}$
3 vn ${setvar}{n}$
4 cz ${class}ℤ$
5 vx ${setvar}{x}$
6 cbs ${class}\mathrm{Base}$
7 1 cv ${setvar}{g}$
8 7 6 cfv ${class}{\mathrm{Base}}_{{g}}$
9 3 cv ${setvar}{n}$
10 cc0 ${class}0$
11 9 10 wceq ${wff}{n}=0$
12 c0g ${class}{0}_{𝑔}$
13 7 12 cfv ${class}{0}_{{g}}$
14 c1 ${class}1$
15 cplusg ${class}{+}_{𝑔}$
16 7 15 cfv ${class}{+}_{{g}}$
17 cn ${class}ℕ$
18 5 cv ${setvar}{x}$
19 18 csn ${class}\left\{{x}\right\}$
20 17 19 cxp ${class}\left(ℕ×\left\{{x}\right\}\right)$
21 16 20 14 cseq ${class}seq1\left({+}_{{g}},\left(ℕ×\left\{{x}\right\}\right)\right)$
22 vs ${setvar}{s}$
23 clt ${class}<$
24 10 9 23 wbr ${wff}0<{n}$
25 22 cv ${setvar}{s}$
26 9 25 cfv ${class}{s}\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 ${class}{s}\left(-{n}\right)$
31 30 28 cfv ${class}{inv}_{g}\left({g}\right)\left({s}\left(-{n}\right)\right)$
32 24 26 31 cif ${class}if\left(0<{n},{s}\left({n}\right),{inv}_{g}\left({g}\right)\left({s}\left(-{n}\right)\right)\right)$
33 22 21 32 csb
34 11 13 33 cif
35 3 5 4 8 34 cmpo
36 1 2 35 cmpt
37 0 36 wceq