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	|- ( ph -> S C_ CC )
	fsumcllem.2	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
	fsumcllem.3	|- ( ph -> A e. Fin )
	fsumcllem.4	|- ( ( ph /\ k e. A ) -> B e. S )
	fsumcllem.5	|- ( ph -> 0 e. S )
Assertion	fsumcllem	|- ( ph -> sum_ k e. A B e. S )

Proof

Step	Hyp	Ref	Expression
1		fsumcllem.1	|- ( ph -> S C_ CC )
2		fsumcllem.2	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
3		fsumcllem.3	|- ( ph -> A e. Fin )
4		fsumcllem.4	|- ( ( ph /\ k e. A ) -> B e. S )
5		fsumcllem.5	|- ( ph -> 0 e. S )
6		simpr	|- ( ( ph /\ A = (/) ) -> A = (/) )
7	6	sumeq1d	|- ( ( ph /\ A = (/) ) -> sum_ k e. A B = sum_ k e. (/) B )
8		sum0	|- sum_ k e. (/) B = 0
9	7 8	syl6eq	|- ( ( ph /\ A = (/) ) -> sum_ k e. A B = 0 )
10	5	adantr	|- ( ( ph /\ A = (/) ) -> 0 e. S )
11	9 10	eqeltrd	|- ( ( ph /\ A = (/) ) -> sum_ k e. A B e. S )
12	1	adantr	|- ( ( ph /\ A =/= (/) ) -> S C_ CC )
13	2	adantlr	|- ( ( ( ph /\ A =/= (/) ) /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
14	3	adantr	|- ( ( ph /\ A =/= (/) ) -> A e. Fin )
15	4	adantlr	|- ( ( ( ph /\ A =/= (/) ) /\ k e. A ) -> B e. S )
16		simpr	|- ( ( ph /\ A =/= (/) ) -> A =/= (/) )
17	12 13 14 15 16	fsumcl2lem	|- ( ( ph /\ A =/= (/) ) -> sum_ k e. A B e. S )
18	11 17	pm2.61dane	|- ( ph -> sum_ k e. A B e. S )