Metamath Proof Explorer


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 ( 𝐹𝑋 ) ) ∈ 𝐵 )