Theorem tsmslem1

Description: The finite partial sums of a function F are defined in a commutative monoid. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	tsmslem1.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tsmslem1.s	⊢ 𝑆 = ( 𝒫 𝐴 ∩ Fin )
	tsmslem1.1	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	tsmslem1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
	tsmslem1.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion	tsmslem1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑋 ) ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		tsmslem1.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		tsmslem1.s	⊢ 𝑆 = ( 𝒫 𝐴 ∩ Fin )
3		tsmslem1.1	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		tsmslem1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
5		tsmslem1.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
6		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → 𝐺 ∈ CMnd )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
9	5	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
10	8 2	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ ( 𝒫 𝐴 ∩ Fin ) )
11		elfpw	⊢ ( 𝑋 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin ) )
12	11	simplbi	⊢ ( 𝑋 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑋 ⊆ 𝐴 )
13	10 12	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ⊆ 𝐴 )
14	9 13	fssresd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ↾ 𝑋 ) : 𝑋 ⟶ 𝐵 )
15	10	elin2d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ Fin )
16		fvexd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( 0g ‘ 𝐺 ) ∈ V )
17	14 15 16	fdmfifsupp	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ↾ 𝑋 ) finSupp ( 0g ‘ 𝐺 ) )
18	1 6 7 8 14 17	gsumcl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑋 ) ) ∈ 𝐵 )