Metamath Proof Explorer

Theorem mulgnegnn

Description: Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 11-Dec-2014)

Ref Expression
Hypotheses mulg1.b 
|- B = ( Base ` G )
mulg1.m 
|- .x. = ( .g ` G )
mulgnegnn.i 
|- I = ( invg ` G )
Assertion mulgnegnn 
|- ( ( N e. NN /\ X e. B ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) )

Proof

Step Hyp Ref Expression
1 mulg1.b 
 |-  B = ( Base ` G )
2 mulg1.m 
 |-  .x. = ( .g ` G )
3 mulgnegnn.i 
 |-  I = ( invg ` G )
4 nncn 
 |-  ( N e. NN -> N e. CC )
5 4 negnegd 
 |-  ( N e. NN -> -u -u N = N )
6 5 adantr 
 |-  ( ( N e. NN /\ X e. B ) -> -u -u N = N )
7 6 fveq2d 
 |-  ( ( N e. NN /\ X e. B ) -> ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u -u N ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) )
8 7 fveq2d 
 |-  ( ( N e. NN /\ X e. B ) -> ( I ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u -u N ) ) = ( I ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) ) )
9 nnnegz 
 |-  ( N e. NN -> -u N e. ZZ )
10 eqid 
 |-  ( +g ` G ) = ( +g ` G )
11 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
12 eqid 
 |-  seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) = seq 1 ( ( +g ` G ) , ( NN X. { X } ) )
13 1 10 11 3 2 12 mulgval 
 |-  ( ( -u N e. ZZ /\ X e. B ) -> ( -u N .x. X ) = if ( -u N = 0 , ( 0g ` G ) , if ( 0 < -u N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) , ( I ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u -u N ) ) ) ) )
14 9 13 sylan 
 |-  ( ( N e. NN /\ X e. B ) -> ( -u N .x. X ) = if ( -u N = 0 , ( 0g ` G ) , if ( 0 < -u N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) , ( I ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u -u N ) ) ) ) )
15 nnne0 
 |-  ( N e. NN -> N =/= 0 )
16 negeq0 
 |-  ( N e. CC -> ( N = 0 <-> -u N = 0 ) )
17 16 necon3abid 
 |-  ( N e. CC -> ( N =/= 0 <-> -. -u N = 0 ) )
18 4 17 syl 
 |-  ( N e. NN -> ( N =/= 0 <-> -. -u N = 0 ) )
19 15 18 mpbid 
 |-  ( N e. NN -> -. -u N = 0 )
20 19 iffalsed 
 |-  ( N e. NN -> if ( -u N = 0 , ( 0g ` G ) , if ( 0 < -u N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) , ( I ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u -u N ) ) ) ) = if ( 0 < -u N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) , ( I ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u -u N ) ) ) )
21 nnre 
 |-  ( N e. NN -> N e. RR )
22 21 renegcld 
 |-  ( N e. NN -> -u N e. RR )
23 nngt0 
 |-  ( N e. NN -> 0 < N )
24 21 lt0neg2d 
 |-  ( N e. NN -> ( 0 < N <-> -u N < 0 ) )
25 23 24 mpbid 
 |-  ( N e. NN -> -u N < 0 )
26 0re 
 |-  0 e. RR
27 ltnsym 
 |-  ( ( -u N e. RR /\ 0 e. RR ) -> ( -u N < 0 -> -. 0 < -u N ) )
28 26 27 mpan2 
 |-  ( -u N e. RR -> ( -u N < 0 -> -. 0 < -u N ) )
29 22 25 28 sylc 
 |-  ( N e. NN -> -. 0 < -u N )
30 29 iffalsed 
 |-  ( N e. NN -> if ( 0 < -u N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) , ( I ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u -u N ) ) ) = ( I ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u -u N ) ) )
31 20 30 eqtrd 
 |-  ( N e. NN -> if ( -u N = 0 , ( 0g ` G ) , if ( 0 < -u N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) , ( I ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u -u N ) ) ) ) = ( I ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u -u N ) ) )
32 31 adantr 
 |-  ( ( N e. NN /\ X e. B ) -> if ( -u N = 0 , ( 0g ` G ) , if ( 0 < -u N , ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u N ) , ( I ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u -u N ) ) ) ) = ( I ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u -u N ) ) )
33 14 32 eqtrd 
 |-  ( ( N e. NN /\ X e. B ) -> ( -u N .x. X ) = ( I ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` -u -u N ) ) )
34 1 10 2 12 mulgnn 
 |-  ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) )
35 34 fveq2d 
 |-  ( ( N e. NN /\ X e. B ) -> ( I ` ( N .x. X ) ) = ( I ` ( seq 1 ( ( +g ` G ) , ( NN X. { X } ) ) ` N ) ) )
36 8 33 35 3eqtr4d 
 |-  ( ( N e. NN /\ X e. B ) -> ( -u N .x. X ) = ( I ` ( N .x. X ) ) )