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

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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgnndir.t ⊢ · = ( .g ‘ 𝐺 )
mulgnndir.p ⊢ + = ( +g ‘ 𝐺 )
Assertion mulgnndir ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 mulgnndir.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgnndir.t ⊢ · = ( .g ‘ 𝐺 )
3 mulgnndir.p ⊢ + = ( +g ‘ 𝐺 )
4 sgrpmgm ⊢ ( 𝐺 ∈ Smgrp → 𝐺 ∈ Mgm )
5 1 3 mgmcl ⊢ ( ( 𝐺 ∈ Mgm ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
6 4 5 syl3an1 ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
7 6 3expb ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
8 7 adantlr ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
9 1 3 sgrpass ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
10 9 adantlr ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
11 simpr2 ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → 𝑁 ∈ ℕ )
12 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
13 11 12 eleqtrdi ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
14 simpr1 ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → 𝑀 ∈ ℕ )
15 14 nnzd ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → 𝑀 ∈ ℤ )
16 eluzadd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑀 ∈ ℤ ) → ( 𝑁 + 𝑀 ) ∈ ( ℤ≥ ‘ ( 1 + 𝑀 ) ) )
17 13 15 16 syl2anc ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑁 + 𝑀 ) ∈ ( ℤ≥ ‘ ( 1 + 𝑀 ) ) )
18 14 nncnd ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → 𝑀 ∈ ℂ )
19 11 nncnd ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → 𝑁 ∈ ℂ )
20 18 19 addcomd ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 + 𝑁 ) = ( 𝑁 + 𝑀 ) )
21 ax-1cn ⊢ 1 ∈ ℂ
22 addcom ⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑀 + 1 ) = ( 1 + 𝑀 ) )
23 18 21 22 sylancl ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 + 1 ) = ( 1 + 𝑀 ) )
24 23 fveq2d ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( ℤ≥ ‘ ( 𝑀 + 1 ) ) = ( ℤ≥ ‘ ( 1 + 𝑀 ) ) )
25 17 20 24 3eltr4d ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 + 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
26 14 12 eleqtrdi ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
27 simpr3 ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
28 elfznn ⊢ ( 𝑥 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) → 𝑥 ∈ ℕ )
29 fvconst2g ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑥 ∈ ℕ ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑥 ) = 𝑋 )
30 27 28 29 syl2an ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑥 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑥 ) = 𝑋 )
31 27 adantr ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑥 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → 𝑋 ∈ 𝐵 )
32 30 31 eqeltrd ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑥 ∈ ( 1 ... ( 𝑀 + 𝑁 ) ) ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑥 ) ∈ 𝐵 )
33 8 10 25 26 32 seqsplit ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ ( 𝑀 + 𝑁 ) ) = ( ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , ( ℕ × { 𝑋 } ) ) ‘ ( 𝑀 + 𝑁 ) ) ) )
34 nnaddcl ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
35 14 11 34 syl2anc ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 + 𝑁 ) ∈ ℕ )
36 eqid ⊢ seq 1 ( + , ( ℕ × { 𝑋 } ) ) = seq 1 ( + , ( ℕ × { 𝑋 } ) )
37 1 3 2 36 mulgnn ⊢ ( ( ( 𝑀 + 𝑁 ) ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ ( 𝑀 + 𝑁 ) ) )
38 35 27 37 syl2anc ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ ( 𝑀 + 𝑁 ) ) )
39 1 3 2 36 mulgnn ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 · 𝑋 ) = ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑀 ) )
40 14 27 39 syl2anc ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 · 𝑋 ) = ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑀 ) )
41 elfznn ⊢ ( 𝑥 ∈ ( 1 ... 𝑁 ) → 𝑥 ∈ ℕ )
42 27 41 29 syl2an ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑥 ) = 𝑋 )
43 27 adantr ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → 𝑋 ∈ 𝐵 )
44 nnaddcl ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 𝑥 + 𝑀 ) ∈ ℕ )
45 41 14 44 syl2anr ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 + 𝑀 ) ∈ ℕ )
46 fvconst2g ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( 𝑥 + 𝑀 ) ∈ ℕ ) → ( ( ℕ × { 𝑋 } ) ‘ ( 𝑥 + 𝑀 ) ) = 𝑋 )
47 43 45 46 syl2anc ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( ( ℕ × { 𝑋 } ) ‘ ( 𝑥 + 𝑀 ) ) = 𝑋 )
48 42 47 eqtr4d ⊢ ( ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑥 ∈ ( 1 ... 𝑁 ) ) → ( ( ℕ × { 𝑋 } ) ‘ 𝑥 ) = ( ( ℕ × { 𝑋 } ) ‘ ( 𝑥 + 𝑀 ) ) )
49 13 15 48 seqshft2 ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) = ( seq ( 1 + 𝑀 ) ( + , ( ℕ × { 𝑋 } ) ) ‘ ( 𝑁 + 𝑀 ) ) )
50 1 3 2 36 mulgnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
51 11 27 50 syl2anc ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑁 · 𝑋 ) = ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
52 23 seqeq1d ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → seq ( 𝑀 + 1 ) ( + , ( ℕ × { 𝑋 } ) ) = seq ( 1 + 𝑀 ) ( + , ( ℕ × { 𝑋 } ) ) )
53 52 20 fveq12d ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( seq ( 𝑀 + 1 ) ( + , ( ℕ × { 𝑋 } ) ) ‘ ( 𝑀 + 𝑁 ) ) = ( seq ( 1 + 𝑀 ) ( + , ( ℕ × { 𝑋 } ) ) ‘ ( 𝑁 + 𝑀 ) ) )
54 49 51 53 3eqtr4d ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑁 · 𝑋 ) = ( seq ( 𝑀 + 1 ) ( + , ( ℕ × { 𝑋 } ) ) ‘ ( 𝑀 + 𝑁 ) ) )
55 40 54 oveq12d ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) = ( ( seq 1 ( + , ( ℕ × { 𝑋 } ) ) ‘ 𝑀 ) + ( seq ( 𝑀 + 1 ) ( + , ( ℕ × { 𝑋 } ) ) ‘ ( 𝑀 + 𝑁 ) ) ) )
56 33 38 55 3eqtr4d ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 + 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑋 ) + ( 𝑁 · 𝑋 ) ) )