Definition df-mulg 12938

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 12937	. 2 class .g
2		vg	. . 3 setvar 𝑔
3		cvv 2737	. . 3 class V
4		vn	. . . 4 setvar 𝑛
5		vx	. . . 4 setvar 𝑥
6		cz 9251	. . . 4 class ℤ
7	2	cv 1352	. . . . 5 class 𝑔
8		cbs 12456	. . . . 5 class Base
9	7, 8	cfv 5216	. . . 4 class (Base‘𝑔)
10	4	cv 1352	. . . . . 6 class 𝑛
11		cc0 7810	. . . . . 6 class 0
12	10, 11	wceq 1353	. . . . 5 wff 𝑛 = 0
13		c0g 12695	. . . . . 6 class 0g
14	7, 13	cfv 5216	. . . . 5 class (0g‘𝑔)
15		vs	. . . . . 6 setvar 𝑠
16		cplusg 12530	. . . . . . . 8 class +g
17	7, 16	cfv 5216	. . . . . . 7 class (+g‘𝑔)
18		cn 8917	. . . . . . . 8 class ℕ
19	5	cv 1352	. . . . . . . . 9 class 𝑥
20	19	csn 3592	. . . . . . . 8 class {𝑥}
21	18, 20	cxp 4624	. . . . . . 7 class (ℕ × {𝑥})
22		c1 7811	. . . . . . 7 class 1
23	17, 21, 22	cseq 10442	. . . . . 6 class seq1((+g‘𝑔), (ℕ × {𝑥}))
24		clt 7990	. . . . . . . 8 class <
25	11, 10, 24	wbr 4003	. . . . . . 7 wff 0 < 𝑛
26	15	cv 1352	. . . . . . . 8 class 𝑠
27	10, 26	cfv 5216	. . . . . . 7 class (𝑠‘𝑛)
28	10	cneg 8127	. . . . . . . . 9 class -𝑛
29	28, 26	cfv 5216	. . . . . . . 8 class (𝑠‘-𝑛)
30		cminusg 12832	. . . . . . . . 9 class invg
31	7, 30	cfv 5216	. . . . . . . 8 class (invg‘𝑔)
32	29, 31	cfv 5216	. . . . . . 7 class ((invg‘𝑔)‘(𝑠‘-𝑛))
33	25, 27, 32	cif 3534	. . . . . 6 class if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))
34	15, 23, 33	csb 3057	. . . . 5 class ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))
35	12, 14, 34	cif 3534	. . . 4 class if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))
36	4, 5, 6, 9, 35	cmpo 5876	. . 3 class (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))))
37	2, 3, 36	cmpt 4064	. 2 class (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))))
38	1, 37	wceq 1353	1 wff .g = (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))))

This definition is referenced by:  mulgfvalg  12939