Definition df-mulg 19039

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 19038	. 2 class .g
2		vg	. . 3 setvar 𝑔
3		cvv 3433	. . 3 class V
4		vn	. . . 4 setvar 𝑛
5		vx	. . . 4 setvar 𝑥
6		cz 12519	. . . 4 class ℤ
7	2	cv 1547	. . . . 5 class 𝑔
8		cbs 17174	. . . . 5 class Base
9	7, 8	cfv 6488	. . . 4 class (Base‘𝑔)
10	4	cv 1547	. . . . . 6 class 𝑛
11		cc0 11034	. . . . . 6 class 0
12	10, 11	wceq 1548	. . . . 5 wff 𝑛 = 0
13		c0g 17397	. . . . . 6 class 0g
14	7, 13	cfv 6488	. . . . 5 class (0g‘𝑔)
15		vs	. . . . . 6 setvar 𝑠
16		cplusg 17215	. . . . . . . 8 class +g
17	7, 16	cfv 6488	. . . . . . 7 class (+g‘𝑔)
18		cn 12169	. . . . . . . 8 class ℕ
19	5	cv 1547	. . . . . . . . 9 class 𝑥
20	19	csn 4557	. . . . . . . 8 class {𝑥}
21	18, 20	cxp 5618	. . . . . . 7 class (ℕ × {𝑥})
22		c1 11035	. . . . . . 7 class 1
23	17, 21, 22	cseq 13958	. . . . . 6 class seq1((+g‘𝑔), (ℕ × {𝑥}))
24		clt 11175	. . . . . . . 8 class <
25	11, 10, 24	wbr 5074	. . . . . . 7 wff 0 < 𝑛
26	15	cv 1547	. . . . . . . 8 class 𝑠
27	10, 26	cfv 6488	. . . . . . 7 class (𝑠‘𝑛)
28	10	cneg 11374	. . . . . . . . 9 class -𝑛
29	28, 26	cfv 6488	. . . . . . . 8 class (𝑠‘-𝑛)
30		cminusg 18905	. . . . . . . . 9 class invg
31	7, 30	cfv 6488	. . . . . . . 8 class (invg‘𝑔)
32	29, 31	cfv 6488	. . . . . . 7 class ((invg‘𝑔)‘(𝑠‘-𝑛))
33	25, 27, 32	cif 4456	. . . . . 6 class if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))
34	15, 23, 33	csb 3832	. . . . 5 class ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))
35	12, 14, 34	cif 4456	. . . 4 class if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))
36	4, 5, 6, 9, 35	cmpo 7361	. . 3 class (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛)))))
37	2, 3, 36	cmpt 5155	. 2 class (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))))
38	1, 37	wceq 1548	1 wff .g = (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))))

This definition is referenced by:  mulgfval  19040  mulgfvalALT  19041