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={\mathrm{Base}}_G$$
	gsumpr12val.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumpr12val.g	$$⊢\phi \to G\in V$$
	gsumpr12val.f	$$⊢\phi \to F:\left\{1,2\right\}⟶B$$
Assertion	gsumpr12val	$$⊢\phi \to {\sum }_{G}F=F\left(1\right)\underset{\dot{}}{+}F\left(2\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsumpr12val.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumpr12val.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		gsumpr12val.g	$$⊢\phi \to G\in V$$
4		gsumpr12val.f	$$⊢\phi \to F:\left\{1,2\right\}⟶B$$
5		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
6		df-2	$$⊢2=1+1$$
7	6	a1i	$$⊢\phi \to 2=1+1$$
8	1 2 3 5 7 4	gsumprval	$$⊢\phi \to {\sum }_{G}F=F\left(1\right)\underset{\dot{}}{+}F\left(2\right)$$