Definition df-mulg

Description: Define the group multiple function, also known as group exponentiation when viewed multiplicatively. (Contributed by Mario Carneiro, 11-Dec-2014)

	Ref	Expression
Assertion	df-mulg	⊢ .g = ( 𝑔 ∈ V ↦ ( 𝑛 ∈ ℤ , 𝑥 ∈ ( Base ‘ 𝑔 ) ↦ if ( 𝑛 = 0 , ( 0g ‘ 𝑔 ) , ⦋ seq 1 ( ( +g ‘ 𝑔 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑔 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmg	⊢ .g
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vn	⊢ 𝑛
4		cz	⊢ ℤ
5		vx	⊢ 𝑥
6		cbs	⊢ Base
7	1	cv	⊢ 𝑔
8	7 6	cfv	⊢ ( Base ‘ 𝑔 )
9	3	cv	⊢ 𝑛
10		cc0	⊢ 0
11	9 10	wceq	⊢ 𝑛 = 0
12		c0g	⊢ 0g
13	7 12	cfv	⊢ ( 0g ‘ 𝑔 )
14		c1	⊢ 1
15		cplusg	⊢ +g
16	7 15	cfv	⊢ ( +g ‘ 𝑔 )
17		cn	⊢ ℕ
18	5	cv	⊢ 𝑥
19	18	csn	⊢ { 𝑥 }
20	17 19	cxp	⊢ ( ℕ × { 𝑥 } )
21	16 20 14	cseq	⊢ seq 1 ( ( +g ‘ 𝑔 ) , ( ℕ × { 𝑥 } ) )
22		vs	⊢ 𝑠
23		clt	⊢ <
24	10 9 23	wbr	⊢ 0 < 𝑛
25	22	cv	⊢ 𝑠
26	9 25	cfv	⊢ ( 𝑠 ‘ 𝑛 )
27		cminusg	⊢ invg
28	7 27	cfv	⊢ ( invg ‘ 𝑔 )
29	9	cneg	⊢ - 𝑛
30	29 25	cfv	⊢ ( 𝑠 ‘ - 𝑛 )
31	30 28	cfv	⊢ ( ( invg ‘ 𝑔 ) ‘ ( 𝑠 ‘ - 𝑛 ) )
32	24 26 31	cif	⊢ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑔 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) )
33	22 21 32	csb	⊢ ⦋ seq 1 ( ( +g ‘ 𝑔 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑔 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) )
34	11 13 33	cif	⊢ if ( 𝑛 = 0 , ( 0g ‘ 𝑔 ) , ⦋ seq 1 ( ( +g ‘ 𝑔 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑔 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) )
35	3 5 4 8 34	cmpo	⊢ ( 𝑛 ∈ ℤ , 𝑥 ∈ ( Base ‘ 𝑔 ) ↦ if ( 𝑛 = 0 , ( 0g ‘ 𝑔 ) , ⦋ seq 1 ( ( +g ‘ 𝑔 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑔 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) ) )
36	1 2 35	cmpt	⊢ ( 𝑔 ∈ V ↦ ( 𝑛 ∈ ℤ , 𝑥 ∈ ( Base ‘ 𝑔 ) ↦ if ( 𝑛 = 0 , ( 0g ‘ 𝑔 ) , ⦋ seq 1 ( ( +g ‘ 𝑔 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑔 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) ) ) )
37	0 36	wceq	⊢ .g = ( 𝑔 ∈ V ↦ ( 𝑛 ∈ ℤ , 𝑥 ∈ ( Base ‘ 𝑔 ) ↦ if ( 𝑛 = 0 , ( 0g ‘ 𝑔 ) , ⦋ seq 1 ( ( +g ‘ 𝑔 ) , ( ℕ × { 𝑥 } ) ) / 𝑠 ⦌ if ( 0 < 𝑛 , ( 𝑠 ‘ 𝑛 ) , ( ( invg ‘ 𝑔 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) ) ) )