Definition df-mulg 18225

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 18224	. 2 class .g
2		vg	. . 3 setvar 𝑔
3		cvv 3494	. . 3 class V
4		vn	. . . 4 setvar 𝑛
5		vx	. . . 4 setvar 𝑥
6		cz 11982	. . . 4 class ℤ
7	2	cv 1536	. . . . 5 class 𝑔
8		cbs 16483	. . . . 5 class Base
9	7, 8	cfv 6355	. . . 4 class (Base‘𝑔)
10	4	cv 1536	. . . . . 6 class 𝑛
11		cc0 10537	. . . . . 6 class 0
12	10, 11	wceq 1537	. . . . 5 wff 𝑛 = 0
13		c0g 16713	. . . . . 6 class 0g
14	7, 13	cfv 6355	. . . . 5 class (0g‘𝑔)
15		vs	. . . . . 6 setvar 𝑠
16		cplusg 16565	. . . . . . . 8 class +g
17	7, 16	cfv 6355	. . . . . . 7 class (+g‘𝑔)
18		cn 11638	. . . . . . . 8 class ℕ
19	5	cv 1536	. . . . . . . . 9 class 𝑥
20	19	csn 4567	. . . . . . . 8 class {𝑥}
21	18, 20	cxp 5553	. . . . . . 7 class (ℕ × {𝑥})
22		c1 10538	. . . . . . 7 class 1
23	17, 21, 22	cseq 13370	. . . . . 6 class seq1((+g‘𝑔), (ℕ × {𝑥}))
24		clt 10675	. . . . . . . 8 class <
25	11, 10, 24	wbr 5066	. . . . . . 7 wff 0 < 𝑛
26	15	cv 1536	. . . . . . . 8 class 𝑠
27	10, 26	cfv 6355	. . . . . . 7 class (𝑠‘𝑛)
28	10	cneg 10871	. . . . . . . . 9 class -𝑛
29	28, 26	cfv 6355	. . . . . . . 8 class (𝑠‘-𝑛)
30		cminusg 18104	. . . . . . . . 9 class invg
31	7, 30	cfv 6355	. . . . . . . 8 class (invg‘𝑔)
32	29, 31	cfv 6355	. . . . . . 7 class ((invg‘𝑔)‘(𝑠‘-𝑛))
33	25, 27, 32	cif 4467	. . . . . 6 class if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))
34	15, 23, 33	csb 3883	. . . . 5 class ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))
35	12, 14, 34	cif 4467	. . . 4 class if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))
36	4, 5, 6, 9, 35	cmpo 7158	. . 3 class (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))))
37	2, 3, 36	cmpt 5146	. 2 class (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))))
38	1, 37	wceq 1537	1 wff .g = (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))))

This definition is referenced by:  mulgfval  18226  mulgfvalALT  18227