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 ) ) ) |
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 ) ) ) |