Theorem fsumcnsrcl

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

	Ref	Expression
Hypotheses	fsumcnsrcl.s	|- ( ph -> S e. ( SubRing ` CCfld ) )
	fsumcnsrcl.a	|- ( ph -> A e. Fin )
	fsumcnsrcl.b	|- ( ( ph /\ k e. A ) -> B e. S )
Assertion	fsumcnsrcl	|- ( ph -> sum_ k e. A B e. S )

Proof

Step	Hyp	Ref	Expression
1		fsumcnsrcl.s	|- ( ph -> S e. ( SubRing ` CCfld ) )
2		fsumcnsrcl.a	|- ( ph -> A e. Fin )
3		fsumcnsrcl.b	|- ( ( ph /\ k e. A ) -> B e. S )
4		cnfldbas	|- CC = ( Base ` CCfld )
5	4	subrgss	|- ( S e. ( SubRing ` CCfld ) -> S C_ CC )
6	1 5	syl	|- ( ph -> S C_ CC )
7		cnfldadd	|- + = ( +g ` CCfld )
8	7	subrgacl	|- ( ( S e. ( SubRing ` CCfld ) /\ a e. S /\ b e. S ) -> ( a + b ) e. S )
9	8	3expb	|- ( ( S e. ( SubRing ` CCfld ) /\ ( a e. S /\ b e. S ) ) -> ( a + b ) e. S )
10	1 9	sylan	|- ( ( ph /\ ( a e. S /\ b e. S ) ) -> ( a + b ) e. S )
11		subrgsubg	|- ( S e. ( SubRing ` CCfld ) -> S e. ( SubGrp ` CCfld ) )
12		cnfld0	|- 0 = ( 0g ` CCfld )
13	12	subg0cl	|- ( S e. ( SubGrp ` CCfld ) -> 0 e. S )
14	1 11 13	3syl	|- ( ph -> 0 e. S )
15	6 10 2 3 14	fsumcllem	|- ( ph -> sum_ k e. A B e. S )