Theorem fsumcnsrcl

Description: Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014)

	Ref	Expression
Hypotheses	fsumcnsrcl.s	$$⊢\phi \to S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
	fsumcnsrcl.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumcnsrcl.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in S$$
Assertion	fsumcnsrcl	$$⊢\phi \to \sum _{k\in A}B\in S$$

Proof

Step	Hyp	Ref	Expression
1		fsumcnsrcl.s	$$⊢\phi \to S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
2		fsumcnsrcl.a	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fsumcnsrcl.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in S$$
4		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
5	4	subrgss	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to S\subseteq ℂ$$
6	1 5	syl	$$⊢\phi \to S\subseteq ℂ$$
7		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
8	7	subrgacl	$$⊢\left(S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge a\in S\wedge b\in S\right)\to a+b\in S$$
9	8	3expb	$$⊢\left(S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge \left(a\in S\wedge b\in S\right)\right)\to a+b\in S$$
10	1 9	sylan	$$⊢\left(\phi \wedge \left(a\in S\wedge b\in S\right)\right)\to a+b\in S$$
11		subrgsubg	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to S\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
12		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
13	12	subg0cl	$$⊢S\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\to 0\in S$$
14	1 11 13	3syl	$$⊢\phi \to 0\in S$$
15	6 10 2 3 14	fsumcllem	$$⊢\phi \to \sum _{k\in A}B\in S$$