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 ) ) )