This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulgz

Description: A group multiple of the identity, for integer multiple. (Contributed by Mario Carneiro, 13-Dec-2014)

Ref Expression
Hypotheses mulgnn0z.b 
|- B = ( Base ` G )
mulgnn0z.t 
|- .x. = ( .g ` G )
mulgnn0z.o 
|- .0. = ( 0g ` G )
Assertion mulgz 
|- ( ( G e. Grp /\ N e. ZZ ) -> ( N .x. .0. ) = .0. )

Proof

Step Hyp Ref Expression
1 mulgnn0z.b 
 |-  B = ( Base ` G )
2 mulgnn0z.t 
 |-  .x. = ( .g ` G )
3 mulgnn0z.o 
 |-  .0. = ( 0g ` G )
4 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
5 4 adantr 
 |-  ( ( G e. Grp /\ N e. ZZ ) -> G e. Mnd )
6 1 2 3 mulgnn0z 
 |-  ( ( G e. Mnd /\ N e. NN0 ) -> ( N .x. .0. ) = .0. )
7 5 6 sylan 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ N e. NN0 ) -> ( N .x. .0. ) = .0. )
8 simpll 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ -u N e. NN0 ) -> G e. Grp )
9 nn0z 
 |-  ( -u N e. NN0 -> -u N e. ZZ )
10 9 adantl 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ -u N e. NN0 ) -> -u N e. ZZ )
11 1 3 grpidcl 
 |-  ( G e. Grp -> .0. e. B )
12 11 ad2antrr 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ -u N e. NN0 ) -> .0. e. B )
13 eqid 
 |-  ( invg ` G ) = ( invg ` G )
14 1 2 13 mulgneg 
 |-  ( ( G e. Grp /\ -u N e. ZZ /\ .0. e. B ) -> ( -u -u N .x. .0. ) = ( ( invg ` G ) ` ( -u N .x. .0. ) ) )
15 8 10 12 14 syl3anc 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ -u N e. NN0 ) -> ( -u -u N .x. .0. ) = ( ( invg ` G ) ` ( -u N .x. .0. ) ) )
16 zcn 
 |-  ( N e. ZZ -> N e. CC )
17 16 ad2antlr 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ -u N e. NN0 ) -> N e. CC )
18 17 negnegd 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ -u N e. NN0 ) -> -u -u N = N )
19 18 oveq1d 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ -u N e. NN0 ) -> ( -u -u N .x. .0. ) = ( N .x. .0. ) )
20 1 2 3 mulgnn0z 
 |-  ( ( G e. Mnd /\ -u N e. NN0 ) -> ( -u N .x. .0. ) = .0. )
21 5 20 sylan 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ -u N e. NN0 ) -> ( -u N .x. .0. ) = .0. )
22 21 fveq2d 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ -u N e. NN0 ) -> ( ( invg ` G ) ` ( -u N .x. .0. ) ) = ( ( invg ` G ) ` .0. ) )
23 3 13 grpinvid 
 |-  ( G e. Grp -> ( ( invg ` G ) ` .0. ) = .0. )
24 23 ad2antrr 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ -u N e. NN0 ) -> ( ( invg ` G ) ` .0. ) = .0. )
25 22 24 eqtrd 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ -u N e. NN0 ) -> ( ( invg ` G ) ` ( -u N .x. .0. ) ) = .0. )
26 15 19 25 3eqtr3d 
 |-  ( ( ( G e. Grp /\ N e. ZZ ) /\ -u N e. NN0 ) -> ( N .x. .0. ) = .0. )
27 elznn0 
 |-  ( N e. ZZ <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) )
28 27 simprbi 
 |-  ( N e. ZZ -> ( N e. NN0 \/ -u N e. NN0 ) )
29 28 adantl 
 |-  ( ( G e. Grp /\ N e. ZZ ) -> ( N e. NN0 \/ -u N e. NN0 ) )
30 7 26 29 mpjaodan 
 |-  ( ( G e. Grp /\ N e. ZZ ) -> ( N .x. .0. ) = .0. )