MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mulg Structured version   Visualization version   GIF version

Definition df-mulg 18165
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 = (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g𝑔), seq1((+g𝑔), (ℕ × {𝑥})) / 𝑠if(0 < 𝑛, (𝑠𝑛), ((invg𝑔)‘(𝑠‘-𝑛))))))
Distinct variable group:   𝑔,𝑛,𝑠,𝑥

Detailed syntax breakdown of Definition df-mulg
StepHypRef Expression
1 cmg 18164 . 2 class .g
2 vg . . 3 setvar 𝑔
3 cvv 3495 . . 3 class V
4 vn . . . 4 setvar 𝑛
5 vx . . . 4 setvar 𝑥
6 cz 11970 . . . 4 class
72cv 1527 . . . . 5 class 𝑔
8 cbs 16473 . . . . 5 class Base
97, 8cfv 6349 . . . 4 class (Base‘𝑔)
104cv 1527 . . . . . 6 class 𝑛
11 cc0 10526 . . . . . 6 class 0
1210, 11wceq 1528 . . . . 5 wff 𝑛 = 0
13 c0g 16703 . . . . . 6 class 0g
147, 13cfv 6349 . . . . 5 class (0g𝑔)
15 vs . . . . . 6 setvar 𝑠
16 cplusg 16555 . . . . . . . 8 class +g
177, 16cfv 6349 . . . . . . 7 class (+g𝑔)
18 cn 11627 . . . . . . . 8 class
195cv 1527 . . . . . . . . 9 class 𝑥
2019csn 4559 . . . . . . . 8 class {𝑥}
2118, 20cxp 5547 . . . . . . 7 class (ℕ × {𝑥})
22 c1 10527 . . . . . . 7 class 1
2317, 21, 22cseq 13359 . . . . . 6 class seq1((+g𝑔), (ℕ × {𝑥}))
24 clt 10664 . . . . . . . 8 class <
2511, 10, 24wbr 5058 . . . . . . 7 wff 0 < 𝑛
2615cv 1527 . . . . . . . 8 class 𝑠
2710, 26cfv 6349 . . . . . . 7 class (𝑠𝑛)
2810cneg 10860 . . . . . . . . 9 class -𝑛
2928, 26cfv 6349 . . . . . . . 8 class (𝑠‘-𝑛)
30 cminusg 18044 . . . . . . . . 9 class invg
317, 30cfv 6349 . . . . . . . 8 class (invg𝑔)
3229, 31cfv 6349 . . . . . . 7 class ((invg𝑔)‘(𝑠‘-𝑛))
3325, 27, 32cif 4465 . . . . . 6 class if(0 < 𝑛, (𝑠𝑛), ((invg𝑔)‘(𝑠‘-𝑛)))
3415, 23, 33csb 3882 . . . . 5 class seq1((+g𝑔), (ℕ × {𝑥})) / 𝑠if(0 < 𝑛, (𝑠𝑛), ((invg𝑔)‘(𝑠‘-𝑛)))
3512, 14, 34cif 4465 . . . 4 class if(𝑛 = 0, (0g𝑔), seq1((+g𝑔), (ℕ × {𝑥})) / 𝑠if(0 < 𝑛, (𝑠𝑛), ((invg𝑔)‘(𝑠‘-𝑛))))
364, 5, 6, 9, 35cmpo 7147 . . 3 class (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g𝑔), seq1((+g𝑔), (ℕ × {𝑥})) / 𝑠if(0 < 𝑛, (𝑠𝑛), ((invg𝑔)‘(𝑠‘-𝑛)))))
372, 3, 36cmpt 5138 . 2 class (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g𝑔), seq1((+g𝑔), (ℕ × {𝑥})) / 𝑠if(0 < 𝑛, (𝑠𝑛), ((invg𝑔)‘(𝑠‘-𝑛))))))
381, 37wceq 1528 1 wff .g = (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g𝑔), seq1((+g𝑔), (ℕ × {𝑥})) / 𝑠if(0 < 𝑛, (𝑠𝑛), ((invg𝑔)‘(𝑠‘-𝑛))))))
Colors of variables: wff setvar class
This definition is referenced by:  mulgfval  18166  mulgfvalALT  18167
  Copyright terms: Public domain W3C validator