This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 ) = ( ( 𝐹 ‘ 𝑀 ) + ( 𝐹 ‘ 𝑁 ) ) )