Theorem gsumprval

Description: Value of the group sum operation over a pair of sequential integers. (Contributed by AV, 14-Dec-2018)

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

Proof

Step	Hyp	Ref	Expression
1		gsumprval.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumprval.p	⊢ + = ( +g ‘ 𝐺 )
3		gsumprval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4		gsumprval.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		gsumprval.n	⊢ ( 𝜑 → 𝑁 = ( 𝑀 + 1 ) )
6		gsumprval.f	⊢ ( 𝜑 → 𝐹 : { 𝑀 , 𝑁 } ⟶ 𝐵 )
7		uzid	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
8	4 7	syl	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
9		peano2uz	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
10	8 9	syl	⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
11		fzpr	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... ( 𝑀 + 1 ) ) = { 𝑀 , ( 𝑀 + 1 ) } )
12	4 11	syl	⊢ ( 𝜑 → ( 𝑀 ... ( 𝑀 + 1 ) ) = { 𝑀 , ( 𝑀 + 1 ) } )
13	5	eqcomd	⊢ ( 𝜑 → ( 𝑀 + 1 ) = 𝑁 )
14	13	preq2d	⊢ ( 𝜑 → { 𝑀 , ( 𝑀 + 1 ) } = { 𝑀 , 𝑁 } )
15	12 14	eqtrd	⊢ ( 𝜑 → ( 𝑀 ... ( 𝑀 + 1 ) ) = { 𝑀 , 𝑁 } )
16	15	feq2d	⊢ ( 𝜑 → ( 𝐹 : ( 𝑀 ... ( 𝑀 + 1 ) ) ⟶ 𝐵 ↔ 𝐹 : { 𝑀 , 𝑁 } ⟶ 𝐵 ) )
17	6 16	mpbird	⊢ ( 𝜑 → 𝐹 : ( 𝑀 ... ( 𝑀 + 1 ) ) ⟶ 𝐵 )
18	1 2 3 10 17	gsumval2	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) )
19		seqp1	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) + ( 𝐹 ‘ ( 𝑀 + 1 ) ) ) )
20	8 19	syl	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑀 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) + ( 𝐹 ‘ ( 𝑀 + 1 ) ) ) )
21		seq1	⊢ ( 𝑀 ∈ ℤ → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
22	4 21	syl	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )
23	13	fveq2d	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑀 + 1 ) ) = ( 𝐹 ‘ 𝑁 ) )
24	22 23	oveq12d	⊢ ( 𝜑 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) + ( 𝐹 ‘ ( 𝑀 + 1 ) ) ) = ( ( 𝐹 ‘ 𝑀 ) + ( 𝐹 ‘ 𝑁 ) ) )
25	18 20 24	3eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐹 ‘ 𝑀 ) + ( 𝐹 ‘ 𝑁 ) ) )