Theorem gsumfsupp

Description: A group sum of a family can be restricted to the support of that family without changing its value, provided that that support is finite. This corresponds to the definition of an (infinite) product in Lang p. 5, last two formulas. (Contributed by AV, 27-Dec-2023)

	Ref	Expression
Hypotheses	gsumfsupp.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumfsupp.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsumfsupp.s	⊢ 𝐼 = ( 𝐹 supp 0 )
	gsumfsupp.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsumfsupp.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsumfsupp.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	gsumfsupp.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion	gsumfsupp	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐼 ) ) = ( 𝐺 Σg 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumfsupp.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumfsupp.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsumfsupp.s	⊢ 𝐼 = ( 𝐹 supp 0 )
4		gsumfsupp.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
5		gsumfsupp.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		gsumfsupp.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7		gsumfsupp.w	⊢ ( 𝜑 → 𝐹 finSupp 0 )
8	3	eqimss2i	⊢ ( 𝐹 supp 0 ) ⊆ 𝐼
9	8	a1i	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐼 )
10	1 2 4 5 6 9 7	gsumres	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐼 ) ) = ( 𝐺 Σg 𝐹 ) )