This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑔 ) ‘ ( 𝑠 ‘ - 𝑛 ) ) ) ) ) )