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 ⊢ ⋅ 𝑔 = g ∈ V ⟼ n ∈ ℤ , x ∈ Base g ⟼ if n = 0 0 g ⦋ seq 1 + g ℕ × x / s⦌ if 0 < n s ⁡ n inv g ⁡ g ⁡ s ⁡ − n

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmg class ⋅ 𝑔
1 vg setvar g
2 cvv class V
3 vn setvar n
4 cz class ℤ
5 vx setvar x
6 cbs class Base
7 1 cv setvar g
8 7 6 cfv class 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 x
20 17 19 cxp class ℕ × x
21 16 20 14 cseq class seq 1 + g ℕ × x
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 ⁡ n
27 cminusg class inv g
28 7 27 cfv class inv g ⁡ g
29 9 cneg class − n
30 29 25 cfv class s ⁡ − n
31 30 28 cfv class inv g ⁡ g ⁡ s ⁡ − n
32 24 26 31 cif class if 0 < n s ⁡ n inv g ⁡ g ⁡ s ⁡ − n
33 22 21 32 csb class ⦋ seq 1 + g ℕ × x / s⦌ if 0 < n s ⁡ n inv g ⁡ g ⁡ s ⁡ − n
34 11 13 33 cif class if n = 0 0 g ⦋ seq 1 + g ℕ × x / s⦌ if 0 < n s ⁡ n inv g ⁡ g ⁡ s ⁡ − n
35 3 5 4 8 34 cmpo class n ∈ ℤ , x ∈ Base g ⟼ if n = 0 0 g ⦋ seq 1 + g ℕ × x / s⦌ if 0 < n s ⁡ n inv g ⁡ g ⁡ s ⁡ − n
36 1 2 35 cmpt class g ∈ V ⟼ n ∈ ℤ , x ∈ Base g ⟼ if n = 0 0 g ⦋ seq 1 + g ℕ × x / s⦌ if 0 < n s ⁡ n inv g ⁡ g ⁡ s ⁡ − n
37 0 36 wceq wff ⋅ 𝑔 = g ∈ V ⟼ n ∈ ℤ , x ∈ Base g ⟼ if n = 0 0 g ⦋ seq 1 + g ℕ × x / s⦌ if 0 < n s ⁡ n inv g ⁡ g ⁡ s ⁡ − n