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 syl5ibr ( ( ( 𝐺 ∈ 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 syl5ibr ( ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) ∧ 𝑛 ∈ ℕ ) → ( ( - 𝑛 · 𝑋 ) = ( 𝑛 · ( 𝐼𝑋 ) ) → ( - - 𝑛 · 𝑋 ) = ( - 𝑛 · ( 𝐼𝑋 ) ) ) )
75 74 ex ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑛 ∈ ℕ → ( ( - 𝑛 · 𝑋 ) = ( 𝑛 · ( 𝐼𝑋 ) ) → ( - - 𝑛 · 𝑋 ) = ( - 𝑛 · ( 𝐼𝑋 ) ) ) ) )
76 9 13 17 21 25 32 62 75 zindd ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵 ) → ( 𝑁 ∈ ℤ → ( - 𝑁 · 𝑋 ) = ( 𝑁 · ( 𝐼𝑋 ) ) ) )
77 76 3impia ( ( 𝐺 ∈ Grp ∧ 𝑋𝐵𝑁 ∈ ℤ ) → ( - 𝑁 · 𝑋 ) = ( 𝑁 · ( 𝐼𝑋 ) ) )
78 77 3com23 ( ( 𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵 ) → ( - 𝑁 · 𝑋 ) = ( 𝑁 · ( 𝐼𝑋 ) ) )