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

Metamath Proof Explorer

Theorem mulgnn0z

Description: A group multiple of the identity, for nonnegative 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 mulgnn0z 
|- ( ( G e. Mnd /\ N e. NN0 ) -> ( 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 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
5 id 
 |-  ( N e. NN -> N e. NN )
6 1 3 mndidcl 
 |-  ( G e. Mnd -> .0. e. B )
7 eqid 
 |-  ( +g ` G ) = ( +g ` G )
8 eqid 
 |-  seq 1 ( ( +g ` G ) , ( NN X. { .0. } ) ) = seq 1 ( ( +g ` G ) , ( NN X. { .0. } ) )
9 1 7 2 8 mulgnn 
 |-  ( ( N e. NN /\ .0. e. B ) -> ( N .x. .0. ) = ( seq 1 ( ( +g ` G ) , ( NN X. { .0. } ) ) ` N ) )
10 5 6 9 syl2anr 
 |-  ( ( G e. Mnd /\ N e. NN ) -> ( N .x. .0. ) = ( seq 1 ( ( +g ` G ) , ( NN X. { .0. } ) ) ` N ) )
11 1 7 3 mndlid 
 |-  ( ( G e. Mnd /\ .0. e. B ) -> ( .0. ( +g ` G ) .0. ) = .0. )
12 6 11 mpdan 
 |-  ( G e. Mnd -> ( .0. ( +g ` G ) .0. ) = .0. )
13 12 adantr 
 |-  ( ( G e. Mnd /\ N e. NN ) -> ( .0. ( +g ` G ) .0. ) = .0. )
14 simpr 
 |-  ( ( G e. Mnd /\ N e. NN ) -> N e. NN )
15 nnuz 
 |-  NN = ( ZZ>= ` 1 )
16 14 15 eleqtrdi 
 |-  ( ( G e. Mnd /\ N e. NN ) -> N e. ( ZZ>= ` 1 ) )
17 6 adantr 
 |-  ( ( G e. Mnd /\ N e. NN ) -> .0. e. B )
18 elfznn 
 |-  ( x e. ( 1 ... N ) -> x e. NN )
19 fvconst2g 
 |-  ( ( .0. e. B /\ x e. NN ) -> ( ( NN X. { .0. } ) ` x ) = .0. )
20 17 18 19 syl2an 
 |-  ( ( ( G e. Mnd /\ N e. NN ) /\ x e. ( 1 ... N ) ) -> ( ( NN X. { .0. } ) ` x ) = .0. )
21 13 16 20 seqid3 
 |-  ( ( G e. Mnd /\ N e. NN ) -> ( seq 1 ( ( +g ` G ) , ( NN X. { .0. } ) ) ` N ) = .0. )
22 10 21 eqtrd 
 |-  ( ( G e. Mnd /\ N e. NN ) -> ( N .x. .0. ) = .0. )
23 oveq1 
 |-  ( N = 0 -> ( N .x. .0. ) = ( 0 .x. .0. ) )
24 1 3 2 mulg0 
 |-  ( .0. e. B -> ( 0 .x. .0. ) = .0. )
25 6 24 syl 
 |-  ( G e. Mnd -> ( 0 .x. .0. ) = .0. )
26 23 25 sylan9eqr 
 |-  ( ( G e. Mnd /\ N = 0 ) -> ( N .x. .0. ) = .0. )
27 22 26 jaodan 
 |-  ( ( G e. Mnd /\ ( N e. NN \/ N = 0 ) ) -> ( N .x. .0. ) = .0. )
28 4 27 sylan2b 
 |-  ( ( G e. Mnd /\ N e. NN0 ) -> ( N .x. .0. ) = .0. )