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 ( 𝑘 ∈ ( 𝑁 ... 𝑃 ) ↦ 𝐵 ) ) + 𝐶 ) )