Metamath Proof Explorer


Theorem gsumnunsn

Description: Closure of a group sum in a non-commutative monoid. (Contributed by Thierry Arnoux, 8-Oct-2018)

Ref Expression
Hypotheses gsumncl.k 𝐾 = ( Base ‘ 𝑀 )
gsumncl.w ( 𝜑𝑀 ∈ Mnd )
gsumncl.p ( 𝜑𝑃 ∈ ( ℤ𝑁 ) )
gsumncl.b ( ( 𝜑𝑘 ∈ ( 𝑁 ... 𝑃 ) ) → 𝐵𝐾 )
gsumnunsn.a + = ( +g𝑀 )
gsumnunsn.l ( 𝜑𝐶𝐾 )
gsumnunsn.c ( ( 𝜑𝑘 = ( 𝑃 + 1 ) ) → 𝐵 = 𝐶 )
Assertion gsumnunsn ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ) = ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ) + 𝐶 ) )

Proof

Step Hyp Ref Expression
1 gsumncl.k 𝐾 = ( Base ‘ 𝑀 )
2 gsumncl.w ( 𝜑𝑀 ∈ Mnd )
3 gsumncl.p ( 𝜑𝑃 ∈ ( ℤ𝑁 ) )
4 gsumncl.b ( ( 𝜑𝑘 ∈ ( 𝑁 ... 𝑃 ) ) → 𝐵𝐾 )
5 gsumnunsn.a + = ( +g𝑀 )
6 gsumnunsn.l ( 𝜑𝐶𝐾 )
7 gsumnunsn.c ( ( 𝜑𝑘 = ( 𝑃 + 1 ) ) → 𝐵 = 𝐶 )
8 seqp1 ( 𝑃 ∈ ( ℤ𝑁 ) → ( seq 𝑁 ( + , ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ) ‘ ( 𝑃 + 1 ) ) = ( ( seq 𝑁 ( + , ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ) ‘ 𝑃 ) + ( ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ‘ ( 𝑃 + 1 ) ) ) )
9 3 8 syl ( 𝜑 → ( seq 𝑁 ( + , ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ) ‘ ( 𝑃 + 1 ) ) = ( ( seq 𝑁 ( + , ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ) ‘ 𝑃 ) + ( ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ‘ ( 𝑃 + 1 ) ) ) )
10 peano2uz ( 𝑃 ∈ ( ℤ𝑁 ) → ( 𝑃 + 1 ) ∈ ( ℤ𝑁 ) )
11 3 10 syl ( 𝜑 → ( 𝑃 + 1 ) ∈ ( ℤ𝑁 ) )
12 4 adantlr ( ( ( 𝜑𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑁 ... 𝑃 ) ) → 𝐵𝐾 )
13 7 adantlr ( ( ( 𝜑𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ) ∧ 𝑘 = ( 𝑃 + 1 ) ) → 𝐵 = 𝐶 )
14 6 ad2antrr ( ( ( 𝜑𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ) ∧ 𝑘 = ( 𝑃 + 1 ) ) → 𝐶𝐾 )
15 13 14 eqeltrd ( ( ( 𝜑𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ) ∧ 𝑘 = ( 𝑃 + 1 ) ) → 𝐵𝐾 )
16 elfzp1 ( 𝑃 ∈ ( ℤ𝑁 ) → ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↔ ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ∨ 𝑘 = ( 𝑃 + 1 ) ) ) )
17 3 16 syl ( 𝜑 → ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↔ ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ∨ 𝑘 = ( 𝑃 + 1 ) ) ) )
18 17 biimpa ( ( 𝜑𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ) → ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ∨ 𝑘 = ( 𝑃 + 1 ) ) )
19 12 15 18 mpjaodan ( ( 𝜑𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ) → 𝐵𝐾 )
20 19 fmpttd ( 𝜑 → ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) : ( 𝑁 ... ( 𝑃 + 1 ) ) ⟶ 𝐾 )
21 1 5 2 11 20 gsumval2 ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ) = ( seq 𝑁 ( + , ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ) ‘ ( 𝑃 + 1 ) ) )
22 4 fmpttd ( 𝜑 → ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) : ( 𝑁 ... 𝑃 ) ⟶ 𝐾 )
23 1 5 2 3 22 gsumval2 ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ) = ( seq 𝑁 ( + , ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ) ‘ 𝑃 ) )
24 fvres ( 𝑖 ∈ ( 𝑁 ... 𝑃 ) → ( ( ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ↾ ( 𝑁 ... 𝑃 ) ) ‘ 𝑖 ) = ( ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ‘ 𝑖 ) )
25 24 adantl ( ( 𝜑𝑖 ∈ ( 𝑁 ... 𝑃 ) ) → ( ( ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ↾ ( 𝑁 ... 𝑃 ) ) ‘ 𝑖 ) = ( ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ‘ 𝑖 ) )
26 fzssp1 ( 𝑁 ... 𝑃 ) ⊆ ( 𝑁 ... ( 𝑃 + 1 ) )
27 resmpt ( ( 𝑁 ... 𝑃 ) ⊆ ( 𝑁 ... ( 𝑃 + 1 ) ) → ( ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ↾ ( 𝑁 ... 𝑃 ) ) = ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) )
28 26 27 ax-mp ( ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ↾ ( 𝑁 ... 𝑃 ) ) = ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 )
29 28 fveq1i ( ( ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ↾ ( 𝑁 ... 𝑃 ) ) ‘ 𝑖 ) = ( ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ‘ 𝑖 )
30 25 29 eqtr3di ( ( 𝜑𝑖 ∈ ( 𝑁 ... 𝑃 ) ) → ( ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ‘ 𝑖 ) = ( ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ‘ 𝑖 ) )
31 3 30 seqfveq ( 𝜑 → ( seq 𝑁 ( + , ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ) ‘ 𝑃 ) = ( seq 𝑁 ( + , ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ) ‘ 𝑃 ) )
32 23 31 eqtr4d ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ) = ( seq 𝑁 ( + , ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ) ‘ 𝑃 ) )
33 eqidd ( 𝜑 → ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) = ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) )
34 eluzfz2 ( ( 𝑃 + 1 ) ∈ ( ℤ𝑁 ) → ( 𝑃 + 1 ) ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) )
35 11 34 syl ( 𝜑 → ( 𝑃 + 1 ) ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) )
36 33 7 35 6 fvmptd ( 𝜑 → ( ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ‘ ( 𝑃 + 1 ) ) = 𝐶 )
37 36 eqcomd ( 𝜑𝐶 = ( ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ‘ ( 𝑃 + 1 ) ) )
38 32 37 oveq12d ( 𝜑 → ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ) + 𝐶 ) = ( ( seq 𝑁 ( + , ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ) ‘ 𝑃 ) + ( ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ‘ ( 𝑃 + 1 ) ) ) )
39 9 21 38 3eqtr4d ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ... ( 𝑃 + 1 ) ) ↦ 𝐵 ) ) = ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ) + 𝐶 ) )