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$$