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