Definition df-mulg 19304

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

Step	Hyp	Ref	Expression
1		cmg 19303	. 2 class .g
2		vg	. . 3 setvar 𝑔
3		cvv 3454	. . 3 class V
4		vn	. . . 4 setvar 𝑛
5		vx	. . . 4 setvar 𝑥
6		cz 12717	. . . 4 class ℤ
7	2	cv 1569	. . . . 5 class 𝑔
8		cbs 17413	. . . . 5 class Base
9	7, 8	cfv 6555	. . . 4 class (Base‘𝑔)
10	4	cv 1569	. . . . . 6 class 𝑛
11		cc0 11224	. . . . . 6 class 0
12	10, 11	wceq 1570	. . . . 5 wff 𝑛 = 0
13		c0g 17636	. . . . . 6 class 0g
14	7, 13	cfv 6555	. . . . 5 class (0g‘𝑔)
15		vs	. . . . . 6 setvar 𝑠
16		cplusg 17454	. . . . . . . 8 class +g
17	7, 16	cfv 6555	. . . . . . 7 class (+g‘𝑔)
18		cn 12359	. . . . . . . 8 class ℕ
19	5	cv 1569	. . . . . . . . 9 class 𝑥
20	19	csn 4588	. . . . . . . 8 class {𝑥}
21	18, 20	cxp 5653	. . . . . . 7 class (ℕ × {𝑥})
22		c1 11225	. . . . . . 7 class 1
23	17, 21, 22	cseq 14168	. . . . . 6 class seq1((+g‘𝑔), (ℕ × {𝑥}))
24		clt 11367	. . . . . . . 8 class <
25	11, 10, 24	wbr 5106	. . . . . . 7 wff 0 < 𝑛
26	15	cv 1569	. . . . . . . 8 class 𝑠
27	10, 26	cfv 6555	. . . . . . 7 class (𝑠‘𝑛)
28	10	cneg 11566	. . . . . . . . 9 class -𝑛
29	28, 26	cfv 6555	. . . . . . . 8 class (𝑠‘ -𝑛)
30		cminusg 19171	. . . . . . . . 9 class invg
31	7, 30	cfv 6555	. . . . . . . 8 class (invg‘𝑔)
32	29, 31	cfv 6555	. . . . . . 7 class ((invg‘𝑔)‘(𝑠‘ -𝑛))
33	25, 27, 32	cif 4485	. . . . . 6 class if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘ -𝑛)))
34	15, 23, 33	csb 3851	. . . . 5 class ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘ -𝑛)))
35	12, 14, 34	cif 4485	. . . 4 class if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘ -𝑛))))
36	4, 5, 6, 9, 35	cmpo 7442	. . 3 class (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘ -𝑛)))))
37	2, 3, 36	cmpt 5189	. 2 class (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘ -𝑛))))))
38	1, 37	wceq 1570	1 wff .g = (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘ -𝑛))))))

This definition is used by:  mulgfval  19305  mulgfvalALT  19306