Metamath Proof Explorer

Theorem mulgneg2

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

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

Proof

Step Hyp Ref Expression
1 mulgneg2.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgneg2.m ⊢ · = ( .g ‘ 𝐺 )
3 mulgneg2.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
4 negeq ⊢ ( 𝑥 = 0 → - 𝑥 = - 0 )
5 neg0 ⊢ - 0 = 0
6 4 5 eqtrdi ⊢ ( 𝑥 = 0 → - 𝑥 = 0 )
7 6 oveq1d ⊢ ( 𝑥 = 0 → ( - 𝑥 · 𝑋 ) = ( 0 · 𝑋 ) )
8 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 · ( 𝐼 ‘ 𝑋 ) ) = ( 0 · ( 𝐼 ‘ 𝑋 ) ) )
9 7 8 eqeq12d ⊢ ( 𝑥 = 0 → ( ( - 𝑥 · 𝑋 ) = ( 𝑥 · ( 𝐼 ‘ 𝑋 ) ) ↔ ( 0 · 𝑋 ) = ( 0 · ( 𝐼 ‘ 𝑋 ) ) ) )
10 negeq ⊢ ( 𝑥 = 𝑛 → - 𝑥 = - 𝑛 )
11 10 oveq1d ⊢ ( 𝑥 = 𝑛 → ( - 𝑥 · 𝑋 ) = ( - 𝑛 · 𝑋 ) )
12 oveq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 · ( 𝐼 ‘ 𝑋 ) ) = ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) )
13 11 12 eqeq12d ⊢ ( 𝑥 = 𝑛 → ( ( - 𝑥 · 𝑋 ) = ( 𝑥 · ( 𝐼 ‘ 𝑋 ) ) ↔ ( - 𝑛 · 𝑋 ) = ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) ) )
14 negeq ⊢ ( 𝑥 = ( 𝑛 + 1 ) → - 𝑥 = - ( 𝑛 + 1 ) )
15 14 oveq1d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( - 𝑥 · 𝑋 ) = ( - ( 𝑛 + 1 ) · 𝑋 ) )
16 oveq1 ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 · ( 𝐼 ‘ 𝑋 ) ) = ( ( 𝑛 + 1 ) · ( 𝐼 ‘ 𝑋 ) ) )
17 15 16 eqeq12d ⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( - 𝑥 · 𝑋 ) = ( 𝑥 · ( 𝐼 ‘ 𝑋 ) ) ↔ ( - ( 𝑛 + 1 ) · 𝑋 ) = ( ( 𝑛 + 1 ) · ( 𝐼 ‘ 𝑋 ) ) ) )
18 negeq ⊢ ( 𝑥 = - 𝑛 → - 𝑥 = - - 𝑛 )
19 18 oveq1d ⊢ ( 𝑥 = - 𝑛 → ( - 𝑥 · 𝑋 ) = ( - - 𝑛 · 𝑋 ) )
20 oveq1 ⊢ ( 𝑥 = - 𝑛 → ( 𝑥 · ( 𝐼 ‘ 𝑋 ) ) = ( - 𝑛 · ( 𝐼 ‘ 𝑋 ) ) )
21 19 20 eqeq12d ⊢ ( 𝑥 = - 𝑛 → ( ( - 𝑥 · 𝑋 ) = ( 𝑥 · ( 𝐼 ‘ 𝑋 ) ) ↔ ( - - 𝑛 · 𝑋 ) = ( - 𝑛 · ( 𝐼 ‘ 𝑋 ) ) ) )
22 negeq ⊢ ( 𝑥 = 𝑁 → - 𝑥 = - 𝑁 )
23 22 oveq1d ⊢ ( 𝑥 = 𝑁 → ( - 𝑥 · 𝑋 ) = ( - 𝑁 · 𝑋 ) )
24 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 · ( 𝐼 ‘ 𝑋 ) ) = ( 𝑁 · ( 𝐼 ‘ 𝑋 ) ) )
25 23 24 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( - 𝑥 · 𝑋 ) = ( 𝑥 · ( 𝐼 ‘ 𝑋 ) ) ↔ ( - 𝑁 · 𝑋 ) = ( 𝑁 · ( 𝐼 ‘ 𝑋 ) ) ) )
26 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
27 1 26 2 mulg0 ⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
28 27 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
29 1 3 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 )
30 1 26 2 mulg0 ⊢ ( ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 → ( 0 · ( 𝐼 ‘ 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
31 29 30 syl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 0 · ( 𝐼 ‘ 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
32 28 31 eqtr4d ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = ( 0 · ( 𝐼 ‘ 𝑋 ) ) )
33 oveq1 ⊢ ( ( - 𝑛 · 𝑋 ) = ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) → ( ( - 𝑛 · 𝑋 ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) = ( ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) )
34 nn0cn ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
35 34 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℂ )
36 ax-1cn ⊢ 1 ∈ ℂ
37 negdi ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → - ( 𝑛 + 1 ) = ( - 𝑛 + - 1 ) )
38 35 36 37 sylancl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → - ( 𝑛 + 1 ) = ( - 𝑛 + - 1 ) )
39 38 oveq1d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( - ( 𝑛 + 1 ) · 𝑋 ) = ( ( - 𝑛 + - 1 ) · 𝑋 ) )
40 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐺 ∈ Grp )
41 nn0negz ⊢ ( 𝑛 ∈ ℕ0 → - 𝑛 ∈ ℤ )
42 41 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → - 𝑛 ∈ ℤ )
43 1z ⊢ 1 ∈ ℤ
44 znegcl ⊢ ( 1 ∈ ℤ → - 1 ∈ ℤ )
45 43 44 mp1i ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → - 1 ∈ ℤ )
46 simplr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
47 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
48 1 2 47 mulgdir ⊢ ( ( 𝐺 ∈ Grp ∧ ( - 𝑛 ∈ ℤ ∧ - 1 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( - 𝑛 + - 1 ) · 𝑋 ) = ( ( - 𝑛 · 𝑋 ) ( +g ‘ 𝐺 ) ( - 1 · 𝑋 ) ) )
49 40 42 45 46 48 syl13anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 𝑛 + - 1 ) · 𝑋 ) = ( ( - 𝑛 · 𝑋 ) ( +g ‘ 𝐺 ) ( - 1 · 𝑋 ) ) )
50 1 2 3 mulgm1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( - 1 · 𝑋 ) = ( 𝐼 ‘ 𝑋 ) )
51 50 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( - 1 · 𝑋 ) = ( 𝐼 ‘ 𝑋 ) )
52 51 oveq2d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 𝑛 · 𝑋 ) ( +g ‘ 𝐺 ) ( - 1 · 𝑋 ) ) = ( ( - 𝑛 · 𝑋 ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) )
53 39 49 52 3eqtrd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( - ( 𝑛 + 1 ) · 𝑋 ) = ( ( - 𝑛 · 𝑋 ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) )
54 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
55 54 ad2antrr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐺 ∈ Mnd )
56 simpr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
57 29 adantr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 )
58 1 2 47 mulgnn0p1 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑛 ∈ ℕ0 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 ) → ( ( 𝑛 + 1 ) · ( 𝐼 ‘ 𝑋 ) ) = ( ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) )
59 55 56 57 58 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 + 1 ) · ( 𝐼 ‘ 𝑋 ) ) = ( ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) )
60 53 59 eqeq12d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - ( 𝑛 + 1 ) · 𝑋 ) = ( ( 𝑛 + 1 ) · ( 𝐼 ‘ 𝑋 ) ) ↔ ( ( - 𝑛 · 𝑋 ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) = ( ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) ) )
61 33 60 imbitrrid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( - 𝑛 · 𝑋 ) = ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) → ( - ( 𝑛 + 1 ) · 𝑋 ) = ( ( 𝑛 + 1 ) · ( 𝐼 ‘ 𝑋 ) ) ) )
62 61 ex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑛 ∈ ℕ0 → ( ( - 𝑛 · 𝑋 ) = ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) → ( - ( 𝑛 + 1 ) · 𝑋 ) = ( ( 𝑛 + 1 ) · ( 𝐼 ‘ 𝑋 ) ) ) ) )
63 fveq2 ⊢ ( ( - 𝑛 · 𝑋 ) = ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) → ( 𝐼 ‘ ( - 𝑛 · 𝑋 ) ) = ( 𝐼 ‘ ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) ) )
64 simpll ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝐺 ∈ Grp )
65 nnnegz ⊢ ( 𝑛 ∈ ℕ → - 𝑛 ∈ ℤ )
66 65 adantl ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → - 𝑛 ∈ ℤ )
67 simplr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → 𝑋 ∈ 𝐵 )
68 1 2 3 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ - 𝑛 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - - 𝑛 · 𝑋 ) = ( 𝐼 ‘ ( - 𝑛 · 𝑋 ) ) )
69 64 66 67 68 syl3anc ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( - - 𝑛 · 𝑋 ) = ( 𝐼 ‘ ( - 𝑛 · 𝑋 ) ) )
70 id ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ )
71 1 2 3 mulgnegnn ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝐵 ) → ( - 𝑛 · ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) ) )
72 70 29 71 syl2anr ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( - 𝑛 · ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) ) )
73 69 72 eqeq12d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( ( - - 𝑛 · 𝑋 ) = ( - 𝑛 · ( 𝐼 ‘ 𝑋 ) ) ↔ ( 𝐼 ‘ ( - 𝑛 · 𝑋 ) ) = ( 𝐼 ‘ ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) ) ) )
74 63 73 imbitrrid ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( ( - 𝑛 · 𝑋 ) = ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) → ( - - 𝑛 · 𝑋 ) = ( - 𝑛 · ( 𝐼 ‘ 𝑋 ) ) ) )
75 74 ex ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑛 ∈ ℕ → ( ( - 𝑛 · 𝑋 ) = ( 𝑛 · ( 𝐼 ‘ 𝑋 ) ) → ( - - 𝑛 · 𝑋 ) = ( - 𝑛 · ( 𝐼 ‘ 𝑋 ) ) ) ) )
76 9 13 17 21 25 32 62 75 zindd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ∈ ℤ → ( - 𝑁 · 𝑋 ) = ( 𝑁 · ( 𝐼 ‘ 𝑋 ) ) ) )
77 76 3impia ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℤ ) → ( - 𝑁 · 𝑋 ) = ( 𝑁 · ( 𝐼 ‘ 𝑋 ) ) )
78 77 3com23 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑁 · 𝑋 ) = ( 𝑁 · ( 𝐼 ‘ 𝑋 ) ) )