This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- B = ( Base ` G )
tsmslem1.s 
|- S = ( ~P A i^i Fin )
tsmslem1.1 
|- ( ph -> G e. CMnd )
tsmslem1.a 
|- ( ph -> A e. W )
tsmslem1.f 
|- ( ph -> F : A --> B )
Assertion tsmslem1 
|- ( ( ph /\ X e. S ) -> ( G gsum ( F |` X ) ) e. B )

Proof

Step Hyp Ref Expression
1 tsmslem1.b 
 |-  B = ( Base ` G )
2 tsmslem1.s 
 |-  S = ( ~P A i^i Fin )
3 tsmslem1.1 
 |-  ( ph -> G e. CMnd )
4 tsmslem1.a 
 |-  ( ph -> A e. W )
5 tsmslem1.f 
 |-  ( ph -> F : A --> B )
6 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
7 3 adantr 
 |-  ( ( ph /\ X e. S ) -> G e. CMnd )
8 simpr 
 |-  ( ( ph /\ X e. S ) -> X e. S )
9 5 adantr 
 |-  ( ( ph /\ X e. S ) -> F : A --> B )
10 8 2 eleqtrdi 
 |-  ( ( ph /\ X e. S ) -> X e. ( ~P A i^i Fin ) )
11 elfpw 
 |-  ( X e. ( ~P A i^i Fin ) <-> ( X C_ A /\ X e. Fin ) )
12 11 simplbi 
 |-  ( X e. ( ~P A i^i Fin ) -> X C_ A )
13 10 12 syl 
 |-  ( ( ph /\ X e. S ) -> X C_ A )
14 9 13 fssresd 
 |-  ( ( ph /\ X e. S ) -> ( F |` X ) : X --> B )
15 10 elin2d 
 |-  ( ( ph /\ X e. S ) -> X e. Fin )
16 fvexd 
 |-  ( ( ph /\ X e. S ) -> ( 0g ` G ) e. _V )
17 14 15 16 fdmfifsupp 
 |-  ( ( ph /\ X e. S ) -> ( F |` X ) finSupp ( 0g ` G ) )
18 1 6 7 8 14 17 gsumcl 
 |-  ( ( ph /\ X e. S ) -> ( G gsum ( F |` X ) ) e. B )