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
|- B = ( Base ` G )
gsumpr12val.p
|- .+ = ( +g ` G )
gsumpr12val.g
|- ( ph -> G e. V )
gsumpr12val.f
|- ( ph -> F : { 1 , 2 } --> B )
Assertion gsumpr12val
|- ( ph -> ( G gsum F ) = ( ( F ` 1 ) .+ ( F ` 2 ) ) )

Proof

Step Hyp Ref Expression
1 gsumpr12val.b
 |-  B = ( Base ` G )
2 gsumpr12val.p
 |-  .+ = ( +g ` G )
3 gsumpr12val.g
 |-  ( ph -> G e. V )
4 gsumpr12val.f
 |-  ( ph -> F : { 1 , 2 } --> B )
5 1zzd
 |-  ( ph -> 1 e. ZZ )
6 df-2
 |-  2 = ( 1 + 1 )
7 6 a1i
 |-  ( ph -> 2 = ( 1 + 1 ) )
8 1 2 3 5 7 4 gsumprval
 |-  ( ph -> ( G gsum F ) = ( ( F ` 1 ) .+ ( F ` 2 ) ) )