# Metamath Proof Explorer

## Theorem fsumcl2lem

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 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}$
fsumcl2lem.5 ${⊢}{\phi }\to {A}\ne \varnothing$
Assertion fsumcl2lem ${⊢}{\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 fsumcl2lem.5 ${⊢}{\phi }\to {A}\ne \varnothing$
6 5 a1d ${⊢}{\phi }\to \left(¬\sum _{{k}\in {A}}{B}\in {S}\to {A}\ne \varnothing \right)$
7 6 necon4bd ${⊢}{\phi }\to \left({A}=\varnothing \to \sum _{{k}\in {A}}{B}\in {S}\right)$
8 sumfc ${⊢}\sum _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)=\sum _{{k}\in {A}}{B}$
9 fveq2 ${⊢}{m}={f}\left({x}\right)\to \left({k}\in {A}⟼{B}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({x}\right)\right)$
10 simprl ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left|{A}\right|\in ℕ$
11 simprr ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}$
12 1 ad2antrr ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {m}\in {A}\right)\to {S}\subseteq ℂ$
13 4 fmpttd ${⊢}{\phi }\to \left({k}\in {A}⟼{B}\right):{A}⟶{S}$
14 13 adantr ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left({k}\in {A}⟼{B}\right):{A}⟶{S}$
15 14 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {m}\in {A}\right)\to \left({k}\in {A}⟼{B}\right)\left({m}\right)\in {S}$
16 12 15 sseldd ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {m}\in {A}\right)\to \left({k}\in {A}⟼{B}\right)\left({m}\right)\in ℂ$
17 f1of ${⊢}{f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\to {f}:\left(1\dots \left|{A}\right|\right)⟶{A}$
18 11 17 syl ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to {f}:\left(1\dots \left|{A}\right|\right)⟶{A}$
19 fvco3 ${⊢}\left({f}:\left(1\dots \left|{A}\right|\right)⟶{A}\wedge {x}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\left({x}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({x}\right)\right)$
20 18 19 sylan ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {x}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\left({x}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({x}\right)\right)$
21 9 10 11 16 20 fsum ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \sum _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)=seq1\left(+,\left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)$
22 8 21 syl5eqr ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \sum _{{k}\in {A}}{B}=seq1\left(+,\left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)$
23 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
24 10 23 eleqtrdi ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left|{A}\right|\in {ℤ}_{\ge 1}$
25 fco ${⊢}\left(\left({k}\in {A}⟼{B}\right):{A}⟶{S}\wedge {f}:\left(1\dots \left|{A}\right|\right)⟶{A}\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right):\left(1\dots \left|{A}\right|\right)⟶{S}$
26 14 18 25 syl2anc ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right):\left(1\dots \left|{A}\right|\right)⟶{S}$
27 26 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge {x}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\left({x}\right)\in {S}$
28 2 adantlr ${⊢}\left(\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}+{y}\in {S}$
29 24 27 28 seqcl ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to seq1\left(+,\left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)\in {S}$
30 22 29 eqeltrd ${⊢}\left({\phi }\wedge \left(\left|{A}\right|\in ℕ\wedge {f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)\to \sum _{{k}\in {A}}{B}\in {S}$
31 30 expr ${⊢}\left({\phi }\wedge \left|{A}\right|\in ℕ\right)\to \left({f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\to \sum _{{k}\in {A}}{B}\in {S}\right)$
32 31 exlimdv ${⊢}\left({\phi }\wedge \left|{A}\right|\in ℕ\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\to \sum _{{k}\in {A}}{B}\in {S}\right)$
33 32 expimpd ${⊢}{\phi }\to \left(\left(\left|{A}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\to \sum _{{k}\in {A}}{B}\in {S}\right)$
34 fz1f1o ${⊢}{A}\in \mathrm{Fin}\to \left({A}=\varnothing \vee \left(\left|{A}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)$
35 3 34 syl ${⊢}{\phi }\to \left({A}=\varnothing \vee \left(\left|{A}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\right)\right)$
36 7 33 35 mpjaod ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}\in {S}$