Metamath Proof Explorer

Theorem mulgnegnn

Description: Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 11-Dec-2014)

Ref Expression
Hypotheses mulg1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulg1.m ⊢ · = ( .g ‘ 𝐺 )
mulgnegnn.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion mulgnegnn ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 mulg1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulg1.m ⊢ · = ( .g ‘ 𝐺 )
3 mulgnegnn.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
4 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
5 4 negnegd ⊢ ( 𝑁 ∈ ℕ → - - 𝑁 = 𝑁 )
6 5 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → - - 𝑁 = 𝑁 )
7 6 fveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - - 𝑁 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
8 7 fveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - - 𝑁 ) ) = ( 𝐼 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) ) )
9 nnnegz ⊢ ( 𝑁 ∈ ℕ → - 𝑁 ∈ ℤ )
10 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
11 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
12 eqid ⊢ seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) )
13 1 10 11 3 2 12 mulgval ⊢ ( ( - 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑁 · 𝑋 ) = if ( - 𝑁 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < - 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) , ( 𝐼 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - - 𝑁 ) ) ) ) )
14 9 13 sylan ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑁 · 𝑋 ) = if ( - 𝑁 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < - 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) , ( 𝐼 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - - 𝑁 ) ) ) ) )
15 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
16 negeq0 ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 = 0 ↔ - 𝑁 = 0 ) )
17 16 necon3abid ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 ≠ 0 ↔ ¬ - 𝑁 = 0 ) )
18 4 17 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ≠ 0 ↔ ¬ - 𝑁 = 0 ) )
19 15 18 mpbid ⊢ ( 𝑁 ∈ ℕ → ¬ - 𝑁 = 0 )
20 19 iffalsed ⊢ ( 𝑁 ∈ ℕ → if ( - 𝑁 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < - 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) , ( 𝐼 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - - 𝑁 ) ) ) ) = if ( 0 < - 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) , ( 𝐼 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - - 𝑁 ) ) ) )
21 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
22 21 renegcld ⊢ ( 𝑁 ∈ ℕ → - 𝑁 ∈ ℝ )
23 nngt0 ⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 )
24 21 lt0neg2d ⊢ ( 𝑁 ∈ ℕ → ( 0 < 𝑁 ↔ - 𝑁 < 0 ) )
25 23 24 mpbid ⊢ ( 𝑁 ∈ ℕ → - 𝑁 < 0 )
26 0re ⊢ 0 ∈ ℝ
27 ltnsym ⊢ ( ( - 𝑁 ∈ ℝ ∧ 0 ∈ ℝ ) → ( - 𝑁 < 0 → ¬ 0 < - 𝑁 ) )
28 26 27 mpan2 ⊢ ( - 𝑁 ∈ ℝ → ( - 𝑁 < 0 → ¬ 0 < - 𝑁 ) )
29 22 25 28 sylc ⊢ ( 𝑁 ∈ ℕ → ¬ 0 < - 𝑁 )
30 29 iffalsed ⊢ ( 𝑁 ∈ ℕ → if ( 0 < - 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) , ( 𝐼 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - - 𝑁 ) ) ) = ( 𝐼 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - - 𝑁 ) ) )
31 20 30 eqtrd ⊢ ( 𝑁 ∈ ℕ → if ( - 𝑁 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < - 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) , ( 𝐼 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - - 𝑁 ) ) ) ) = ( 𝐼 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - - 𝑁 ) ) )
32 31 adantr ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → if ( - 𝑁 = 0 , ( 0g ‘ 𝐺 ) , if ( 0 < - 𝑁 , ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - 𝑁 ) , ( 𝐼 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - - 𝑁 ) ) ) ) = ( 𝐼 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - - 𝑁 ) ) )
33 14 32 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ - - 𝑁 ) ) )
34 1 10 2 12 mulgnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
35 34 fveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝐼 ‘ ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) ) )
36 8 33 35 3eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑁 · 𝑋 ) = ( 𝐼 ‘ ( 𝑁 · 𝑋 ) ) )