Definition df-mulg 18768

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 18767	. 2 class .g
2		vg	. . 3 setvar 𝑔
3		cvv 3441	. . 3 class V
4		vn	. . . 4 setvar 𝑛
5		vx	. . . 4 setvar 𝑥
6		cz 12389	. . . 4 class ℤ
7	2	cv 1539	. . . . 5 class 𝑔
8		cbs 16979	. . . . 5 class Base
9	7, 8	cfv 6463	. . . 4 class (Base‘𝑔)
10	4	cv 1539	. . . . . 6 class 𝑛
11		cc0 10941	. . . . . 6 class 0
12	10, 11	wceq 1540	. . . . 5 wff 𝑛 = 0
13		c0g 17217	. . . . . 6 class 0g
14	7, 13	cfv 6463	. . . . 5 class (0g‘𝑔)
15		vs	. . . . . 6 setvar 𝑠
16		cplusg 17029	. . . . . . . 8 class +g
17	7, 16	cfv 6463	. . . . . . 7 class (+g‘𝑔)
18		cn 12043	. . . . . . . 8 class ℕ
19	5	cv 1539	. . . . . . . . 9 class 𝑥
20	19	csn 4569	. . . . . . . 8 class {𝑥}
21	18, 20	cxp 5603	. . . . . . 7 class (ℕ × {𝑥})
22		c1 10942	. . . . . . 7 class 1
23	17, 21, 22	cseq 13791	. . . . . 6 class seq1((+g‘𝑔), (ℕ × {𝑥}))
24		clt 11079	. . . . . . . 8 class <
25	11, 10, 24	wbr 5085	. . . . . . 7 wff 0 < 𝑛
26	15	cv 1539	. . . . . . . 8 class 𝑠
27	10, 26	cfv 6463	. . . . . . 7 class (𝑠‘𝑛)
28	10	cneg 11276	. . . . . . . . 9 class -𝑛
29	28, 26	cfv 6463	. . . . . . . 8 class (𝑠‘-𝑛)
30		cminusg 18645	. . . . . . . . 9 class invg
31	7, 30	cfv 6463	. . . . . . . 8 class (invg‘𝑔)
32	29, 31	cfv 6463	. . . . . . 7 class ((invg‘𝑔)‘(𝑠‘-𝑛))
33	25, 27, 32	cif 4469	. . . . . 6 class if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))
34	15, 23, 33	csb 3841	. . . . 5 class ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))
35	12, 14, 34	cif 4469	. . . 4 class if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))
36	4, 5, 6, 9, 35	cmpo 7315	. . 3 class (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))))
37	2, 3, 36	cmpt 5168	. 2 class (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))))
38	1, 37	wceq 1540	1 wff .g = (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))))

This definition is referenced by:  mulgfval  18769  mulgfvalALT  18770