Metamath Proof Explorer

Theorem gsumsplit1r

Description: Splitting off the rightmost summand of a group sum. This corresponds to the (inductive) definition of a (finite) product in Lang p. 4, first formula. (Contributed by AV, 26-Dec-2023)

Ref Expression
Hypotheses gsumsplit1r.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumsplit1r.p ⊢ + = ( +g ‘ 𝐺 )
gsumsplit1r.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
gsumsplit1r.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
gsumsplit1r.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
gsumsplit1r.f ⊢ ( 𝜑 → 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ 𝐵 )
Assertion gsumsplit1r ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumsplit1r.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumsplit1r.p ⊢ + = ( +g ‘ 𝐺 )
3 gsumsplit1r.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4 gsumsplit1r.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5 gsumsplit1r.n ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
6 gsumsplit1r.f ⊢ ( 𝜑 → 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ 𝐵 )
7 peano2uz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
8 5 7 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
9 1 2 3 8 6 gsumval2 ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) )
10 seqp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
11 5 10 syl ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
12 fzssp1 ⊢ ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) )
13 12 a1i ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ⊆ ( 𝑀 ... ( 𝑁 + 1 ) ) )
14 6 13 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) : ( 𝑀 ... 𝑁 ) ⟶ 𝐵 )
15 1 2 3 5 14 gsumval2 ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) ) = ( seq 𝑀 ( + , ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) ) ‘ 𝑁 ) )
16 4 uzidd ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
17 seq1 ⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) ) ‘ 𝑀 ) = ( ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) ‘ 𝑀 ) )
18 4 17 syl ⊢ ( 𝜑 → ( seq 𝑀 ( + , ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) ) ‘ 𝑀 ) = ( ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) ‘ 𝑀 ) )
19 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
20 5 19 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
21 20 fvresd ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
22 18 21 eqtrd ⊢ ( 𝜑 → ( seq 𝑀 ( + , ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
23 fzp1ss ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
24 4 23 syl ⊢ ( 𝜑 → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
25 24 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
26 25 fvresd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
27 16 22 5 26 seqfveq2 ⊢ ( 𝜑 → ( seq 𝑀 ( + , ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
28 15 27 eqtr2d ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) ) )
29 28 oveq1d ⊢ ( 𝜑 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) = ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )
30 9 11 29 3eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑀 ... 𝑁 ) ) ) + ( 𝐹 ‘ ( 𝑁 + 1 ) ) ) )