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