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 
|- .x. = ( .g ` G )
mulgneg2.i 
|- I = ( invg ` G )
Assertion mulgneg2 
|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( -u N .x. X ) = ( N .x. ( I ` X ) ) )

Proof

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