Metamath Proof Explorer

Theorem mulgneg

Description: Group multiple (exponentiation) operation at a negative integer. (Contributed by Paul Chapman, 17-Apr-2009) (Revised by Mario Carneiro, 11-Dec-2014)

Ref Expression
Hypotheses mulgnncl.b 
|- B = ( Base ` G )
mulgnncl.t 
|- .x. = ( .g ` G )
mulgneg.i 
|- I = ( invg ` G )
Assertion mulgneg 
|- ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) )

Proof

Step Hyp Ref Expression
1 mulgnncl.b 
 |-  B = ( Base ` G )
2 mulgnncl.t 
 |-  .x. = ( .g ` G )
3 mulgneg.i 
 |-  I = ( invg ` G )
4 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
5 simpr 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N e. NN ) -> N e. NN )
6 simpl3 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N e. NN ) -> X e. B )
7 1 2 3 mulgnegnn 
 |-  ( ( N e. NN /\ X e. B ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) )
8 5 6 7 syl2anc 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N e. NN ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) )
9 simpl1 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> G e. Grp )
10 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
11 10 3 grpinvid 
 |-  ( G e. Grp -> ( I ` ( 0g ` G ) ) = ( 0g ` G ) )
12 9 11 syl 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( I ` ( 0g ` G ) ) = ( 0g ` G ) )
13 simpr 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> N = 0 )
14 13 oveq1d 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( N .x. X ) = ( 0 .x. X ) )
15 simpl3 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> X e. B )
16 1 10 2 mulg0 
 |-  ( X e. B -> ( 0 .x. X ) = ( 0g ` G ) )
17 15 16 syl 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( 0 .x. X ) = ( 0g ` G ) )
18 14 17 eqtrd 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( N .x. X ) = ( 0g ` G ) )
19 18 fveq2d 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( I ` ( N .x. X ) ) = ( I ` ( 0g ` G ) ) )
20 13 negeqd 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> -u N = -u 0 )
21 neg0 
 |-  -u 0 = 0
22 20 21 eqtrdi 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> -u N = 0 )
23 22 oveq1d 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( -u N .x. X ) = ( 0 .x. X ) )
24 23 17 eqtrd 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( -u N .x. X ) = ( 0g ` G ) )
25 12 19 24 3eqtr4rd 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N = 0 ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) )
26 8 25 jaodan 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. NN \/ N = 0 ) ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) )
27 4 26 sylan2b 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ N e. NN0 ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) )
28 simpl1 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> G e. Grp )
29 simprr 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. NN )
30 29 nnzd 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. ZZ )
31 simpl3 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> X e. B )
32 1 2 mulgcl 
 |-  ( ( G e. Grp /\ -u N e. ZZ /\ X e. B ) -> ( -u N .x. X ) e. B )
33 28 30 31 32 syl3anc 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u N .x. X ) e. B )
34 1 3 grpinvinv 
 |-  ( ( G e. Grp /\ ( -u N .x. X ) e. B ) -> ( I ` ( I ` ( -u N .x. X ) ) ) = ( -u N .x. X ) )
35 28 33 34 syl2anc 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( I ` ( I ` ( -u N .x. X ) ) ) = ( -u N .x. X ) )
36 1 2 3 mulgnegnn 
 |-  ( ( -u N e. NN /\ X e. B ) -> ( -u -u N .x. X ) = ( I ` ( -u N .x. X ) ) )
37 29 31 36 syl2anc 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u -u N .x. X ) = ( I ` ( -u N .x. X ) ) )
38 simprl 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> N e. RR )
39 38 recnd 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> N e. CC )
40 39 negnegd 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u -u N = N )
41 40 oveq1d 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u -u N .x. X ) = ( N .x. X ) )
42 37 41 eqtr3d 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( I ` ( -u N .x. X ) ) = ( N .x. X ) )
43 42 fveq2d 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( I ` ( I ` ( -u N .x. X ) ) ) = ( I ` ( N .x. X ) ) )
44 35 43 eqtr3d 
 |-  ( ( ( G e. Grp /\ N e. ZZ /\ X e. B ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) )
45 simp2 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> N e. ZZ )
46 elznn0nn 
 |-  ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
47 45 46 sylib 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
48 27 44 47 mpjaodan 
 |-  ( ( G e. Grp /\ N e. ZZ /\ X e. B ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) )