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