# Metamath Proof Explorer

## Theorem fsumcllem

Description: - Lemma for finite sum closures. (The "-" before "Lemma" forces the math content to be displayed in the Statement List - NM 11-Feb-2008.) (Contributed by NM, 9-Nov-2005) (Revised by Mario Carneiro, 3-Jun-2014)

Ref Expression
Hypotheses fsumcllem.1 ${⊢}{\phi }\to {S}\subseteq ℂ$
fsumcllem.2 ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}+{y}\in {S}$
fsumcllem.3 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fsumcllem.4 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in {S}$
fsumcllem.5 ${⊢}{\phi }\to 0\in {S}$
Assertion fsumcllem ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}\in {S}$

### Proof

Step Hyp Ref Expression
1 fsumcllem.1 ${⊢}{\phi }\to {S}\subseteq ℂ$
2 fsumcllem.2 ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}+{y}\in {S}$
3 fsumcllem.3 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
4 fsumcllem.4 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in {S}$
5 fsumcllem.5 ${⊢}{\phi }\to 0\in {S}$
6 simpr ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to {A}=\varnothing$
7 6 sumeq1d ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to \sum _{{k}\in {A}}{B}=\sum _{{k}\in \varnothing }{B}$
8 sum0 ${⊢}\sum _{{k}\in \varnothing }{B}=0$
9 7 8 syl6eq ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to \sum _{{k}\in {A}}{B}=0$
10 5 adantr ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to 0\in {S}$
11 9 10 eqeltrd ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to \sum _{{k}\in {A}}{B}\in {S}$
12 1 adantr ${⊢}\left({\phi }\wedge {A}\ne \varnothing \right)\to {S}\subseteq ℂ$
13 2 adantlr ${⊢}\left(\left({\phi }\wedge {A}\ne \varnothing \right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}+{y}\in {S}$
14 3 adantr ${⊢}\left({\phi }\wedge {A}\ne \varnothing \right)\to {A}\in \mathrm{Fin}$
15 4 adantlr ${⊢}\left(\left({\phi }\wedge {A}\ne \varnothing \right)\wedge {k}\in {A}\right)\to {B}\in {S}$
16 simpr ${⊢}\left({\phi }\wedge {A}\ne \varnothing \right)\to {A}\ne \varnothing$
17 12 13 14 15 16 fsumcl2lem ${⊢}\left({\phi }\wedge {A}\ne \varnothing \right)\to \sum _{{k}\in {A}}{B}\in {S}$
18 11 17 pm2.61dane ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}\in {S}$