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

Metamath Proof Explorer

Theorem gsumpr12val

Description: Value of the group sum operation over the pair { 1 , 2 } . (Contributed by AV, 14-Dec-2018)

Ref Expression
Hypotheses gsumpr12val.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumpr12val.p ⊢ + = ( +g ‘ 𝐺 )
gsumpr12val.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
gsumpr12val.f ⊢ ( 𝜑 → 𝐹 : { 1 , 2 } ⟶ 𝐵 )
Assertion gsumpr12val ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐹 ‘ 1 ) + ( 𝐹 ‘ 2 ) ) )

Proof

Step Hyp Ref Expression
1 gsumpr12val.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumpr12val.p ⊢ + = ( +g ‘ 𝐺 )
3 gsumpr12val.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
4 gsumpr12val.f ⊢ ( 𝜑 → 𝐹 : { 1 , 2 } ⟶ 𝐵 )
5 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
6 df-2 ⊢ 2 = ( 1 + 1 )
7 6 a1i ⊢ ( 𝜑 → 2 = ( 1 + 1 ) )
8 1 2 3 5 7 4 gsumprval ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐹 ‘ 1 ) + ( 𝐹 ‘ 2 ) ) )