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 B = Base G
gsumsplit1r.p + ˙ = + G
gsumsplit1r.g φ G V
gsumsplit1r.m φ M
gsumsplit1r.n φ N M
gsumsplit1r.f φ F : M N + 1 B
Assertion gsumsplit1r φ G F = G F M N + ˙ F N + 1

Proof

Step Hyp Ref Expression
1 gsumsplit1r.b B = Base G
2 gsumsplit1r.p + ˙ = + G
3 gsumsplit1r.g φ G V
4 gsumsplit1r.m φ M
5 gsumsplit1r.n φ N M
6 gsumsplit1r.f φ F : M N + 1 B
7 peano2uz N M N + 1 M
8 5 7 syl φ N + 1 M
9 1 2 3 8 6 gsumval2 φ G F = seq M + ˙ F N + 1
10 seqp1 N M seq M + ˙ F N + 1 = seq M + ˙ F N + ˙ F N + 1
11 5 10 syl φ seq M + ˙ F N + 1 = seq M + ˙ F N + ˙ F N + 1
12 fzssp1 M N M N + 1
13 12 a1i φ M N M N + 1
14 6 13 fssresd φ F M N : M N B
15 1 2 3 5 14 gsumval2 φ G F M N = seq M + ˙ F M N N
16 4 uzidd φ M M
17 seq1 M seq M + ˙ F M N M = F M N M
18 4 17 syl φ seq M + ˙ F M N M = F M N M
19 eluzfz1 N M M M N
20 5 19 syl φ M M N
21 20 fvresd φ F M N M = F M
22 18 21 eqtrd φ seq M + ˙ F M N M = F M
23 fzp1ss M M + 1 N M N
24 4 23 syl φ M + 1 N M N
25 24 sselda φ x M + 1 N x M N
26 25 fvresd φ x M + 1 N F M N x = F x
27 16 22 5 26 seqfveq2 φ seq M + ˙ F M N N = seq M + ˙ F N
28 15 27 eqtr2d φ seq M + ˙ F N = G F M N
29 28 oveq1d φ seq M + ˙ F N + ˙ F N + 1 = G F M N + ˙ F N + 1
30 9 11 29 3eqtrd φ G F = G F M N + ˙ F N + 1