Metamath Proof Explorer

Theorem mulgnndir

Description: Sum of group multiples, for positive multiples. (Contributed by Mario Carneiro, 11-Dec-2014) (Revised by AV, 29-Aug-2021)

Ref Expression
Hypotheses mulgnndir.b 
|- B = ( Base ` G )
mulgnndir.t 
|- .x. = ( .g ` G )
mulgnndir.p 
|- .+ = ( +g ` G )
Assertion mulgnndir 
|- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )

Proof

Step Hyp Ref Expression
1 mulgnndir.b 
 |-  B = ( Base ` G )
2 mulgnndir.t 
 |-  .x. = ( .g ` G )
3 mulgnndir.p 
 |-  .+ = ( +g ` G )
4 sgrpmgm 
 |-  ( G e. Smgrp -> G e. Mgm )
5 1 3 mgmcl 
 |-  ( ( G e. Mgm /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
6 4 5 syl3an1 
 |-  ( ( G e. Smgrp /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
7 6 3expb 
 |-  ( ( G e. Smgrp /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
8 7 adantlr 
 |-  ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ ( x e. B /\ y e. B ) ) -> ( x .+ y ) e. B )
9 1 3 sgrpass 
 |-  ( ( G e. Smgrp /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
10 9 adantlr 
 |-  ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
11 simpr2 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> N e. NN )
12 nnuz 
 |-  NN = ( ZZ>= ` 1 )
13 11 12 eleqtrdi 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> N e. ( ZZ>= ` 1 ) )
14 simpr1 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> M e. NN )
15 14 nnzd 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> M e. ZZ )
16 eluzadd 
 |-  ( ( N e. ( ZZ>= ` 1 ) /\ M e. ZZ ) -> ( N + M ) e. ( ZZ>= ` ( 1 + M ) ) )
17 13 15 16 syl2anc 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( N + M ) e. ( ZZ>= ` ( 1 + M ) ) )
18 14 nncnd 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> M e. CC )
19 11 nncnd 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> N e. CC )
20 18 19 addcomd 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M + N ) = ( N + M ) )
21 ax-1cn 
 |-  1 e. CC
22 addcom 
 |-  ( ( M e. CC /\ 1 e. CC ) -> ( M + 1 ) = ( 1 + M ) )
23 18 21 22 sylancl 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M + 1 ) = ( 1 + M ) )
24 23 fveq2d 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ZZ>= ` ( M + 1 ) ) = ( ZZ>= ` ( 1 + M ) ) )
25 17 20 24 3eltr4d 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M + N ) e. ( ZZ>= ` ( M + 1 ) ) )
26 14 12 eleqtrdi 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> M e. ( ZZ>= ` 1 ) )
27 simpr3 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> X e. B )
28 elfznn 
 |-  ( x e. ( 1 ... ( M + N ) ) -> x e. NN )
29 fvconst2g 
 |-  ( ( X e. B /\ x e. NN ) -> ( ( NN X. { X } ) ` x ) = X )
30 27 28 29 syl2an 
 |-  ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... ( M + N ) ) ) -> ( ( NN X. { X } ) ` x ) = X )
31 27 adantr 
 |-  ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... ( M + N ) ) ) -> X e. B )
32 30 31 eqeltrd 
 |-  ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... ( M + N ) ) ) -> ( ( NN X. { X } ) ` x ) e. B )
33 8 10 25 26 32 seqsplit 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( seq 1 ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) = ( ( seq 1 ( .+ , ( NN X. { X } ) ) ` M ) .+ ( seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) ) )
34 nnaddcl 
 |-  ( ( M e. NN /\ N e. NN ) -> ( M + N ) e. NN )
35 14 11 34 syl2anc 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M + N ) e. NN )
36 eqid 
 |-  seq 1 ( .+ , ( NN X. { X } ) ) = seq 1 ( .+ , ( NN X. { X } ) )
37 1 3 2 36 mulgnn 
 |-  ( ( ( M + N ) e. NN /\ X e. B ) -> ( ( M + N ) .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) )
38 35 27 37 syl2anc 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) )
39 1 3 2 36 mulgnn 
 |-  ( ( M e. NN /\ X e. B ) -> ( M .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` M ) )
40 14 27 39 syl2anc 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( M .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` M ) )
41 elfznn 
 |-  ( x e. ( 1 ... N ) -> x e. NN )
42 27 41 29 syl2an 
 |-  ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> ( ( NN X. { X } ) ` x ) = X )
43 27 adantr 
 |-  ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> X e. B )
44 nnaddcl 
 |-  ( ( x e. NN /\ M e. NN ) -> ( x + M ) e. NN )
45 41 14 44 syl2anr 
 |-  ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> ( x + M ) e. NN )
46 fvconst2g 
 |-  ( ( X e. B /\ ( x + M ) e. NN ) -> ( ( NN X. { X } ) ` ( x + M ) ) = X )
47 43 45 46 syl2anc 
 |-  ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> ( ( NN X. { X } ) ` ( x + M ) ) = X )
48 42 47 eqtr4d 
 |-  ( ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) /\ x e. ( 1 ... N ) ) -> ( ( NN X. { X } ) ` x ) = ( ( NN X. { X } ) ` ( x + M ) ) )
49 13 15 48 seqshft2 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) = ( seq ( 1 + M ) ( .+ , ( NN X. { X } ) ) ` ( N + M ) ) )
50 1 3 2 36 mulgnn 
 |-  ( ( N e. NN /\ X e. B ) -> ( N .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) )
51 11 27 50 syl2anc 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( N .x. X ) = ( seq 1 ( .+ , ( NN X. { X } ) ) ` N ) )
52 23 seqeq1d 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) = seq ( 1 + M ) ( .+ , ( NN X. { X } ) ) )
53 52 20 fveq12d 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) = ( seq ( 1 + M ) ( .+ , ( NN X. { X } ) ) ` ( N + M ) ) )
54 49 51 53 3eqtr4d 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( N .x. X ) = ( seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) )
55 40 54 oveq12d 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M .x. X ) .+ ( N .x. X ) ) = ( ( seq 1 ( .+ , ( NN X. { X } ) ) ` M ) .+ ( seq ( M + 1 ) ( .+ , ( NN X. { X } ) ) ` ( M + N ) ) ) )
56 33 38 55 3eqtr4d 
 |-  ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) )