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