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 ⊢B=BaseG
mulgneg2.m ⊢·˙=⋅G
mulgneg2.i ⊢I=invg⁡G
Assertion mulgneg2 ⊢G∈Grp∧N∈ℤ∧X∈B→- N·˙X=N·˙I⁡X

Proof

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