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