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 = Base G
mulgneg2.m · ˙ = G
mulgneg2.i I = inv g G
Assertion mulgneg2 G Grp N X B -N · ˙ X = N · ˙ I X

Proof

Step Hyp Ref Expression
1 mulgneg2.b B = Base G
2 mulgneg2.m · ˙ = G
3 mulgneg2.i I = inv g 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 0 G = 0 G
27 1 26 2 mulg0 X B 0 · ˙ X = 0 G
28 27 adantl G Grp X B 0 · ˙ X = 0 G
29 1 3 grpinvcl G Grp X B I X B
30 1 26 2 mulg0 I X B 0 · ˙ I X = 0 G
31 29 30 syl G Grp X B 0 · ˙ I X = 0 G
32 28 31 eqtr4d G Grp X B 0 · ˙ X = 0 · ˙ I X
33 oveq1 n · ˙ X = n · ˙ I X n · ˙ X + G I X = n · ˙ I X + G I 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 + G I X
53 39 49 52 3eqtrd G Grp X B n 0 n + 1 · ˙ X = n · ˙ X + G I 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 + G I X
59 55 56 57 58 syl3anc G Grp X B n 0 n + 1 · ˙ I X = n · ˙ I X + G I X
60 53 59 eqeq12d G Grp X B n 0 n + 1 · ˙ X = n + 1 · ˙ I X n · ˙ X + G I X = n · ˙ I X + G I X
61 33 60 syl5ibr 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 syl5ibr 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