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 ( 𝜑𝑆 ⊆ ℂ )
fsumcllem.2 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
fsumcllem.3 ( 𝜑𝐴 ∈ Fin )
fsumcllem.4 ( ( 𝜑𝑘𝐴 ) → 𝐵𝑆 )
fsumcl2lem.5 ( 𝜑𝐴 ≠ ∅ )
Assertion fsumcl2lem ( 𝜑 → Σ 𝑘𝐴 𝐵𝑆 )

Proof

Step Hyp Ref Expression
1 fsumcllem.1 ( 𝜑𝑆 ⊆ ℂ )
2 fsumcllem.2 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
3 fsumcllem.3 ( 𝜑𝐴 ∈ Fin )
4 fsumcllem.4 ( ( 𝜑𝑘𝐴 ) → 𝐵𝑆 )
5 fsumcl2lem.5 ( 𝜑𝐴 ≠ ∅ )
6 5 a1d ( 𝜑 → ( ¬ Σ 𝑘𝐴 𝐵𝑆𝐴 ≠ ∅ ) )
7 6 necon4bd ( 𝜑 → ( 𝐴 = ∅ → Σ 𝑘𝐴 𝐵𝑆 ) )
8 sumfc Σ 𝑚𝐴 ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) = Σ 𝑘𝐴 𝐵
9 fveq2 ( 𝑚 = ( 𝑓𝑥 ) → ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝑓𝑥 ) ) )
10 simprl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
11 simprr ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 )
12 1 ad2antrr ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) ∧ 𝑚𝐴 ) → 𝑆 ⊆ ℂ )
13 4 fmpttd ( 𝜑 → ( 𝑘𝐴𝐵 ) : 𝐴𝑆 )
14 13 adantr ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → ( 𝑘𝐴𝐵 ) : 𝐴𝑆 )
15 14 ffvelrnda ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) ∧ 𝑚𝐴 ) → ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) ∈ 𝑆 )
16 12 15 sseldd ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) ∧ 𝑚𝐴 ) → ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) ∈ ℂ )
17 f1of ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
18 11 17 syl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
19 fvco3 ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) ‘ 𝑥 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝑓𝑥 ) ) )
20 18 19 sylan ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) ‘ 𝑥 ) = ( ( 𝑘𝐴𝐵 ) ‘ ( 𝑓𝑥 ) ) )
21 9 10 11 16 20 fsum ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → Σ 𝑚𝐴 ( ( 𝑘𝐴𝐵 ) ‘ 𝑚 ) = ( seq 1 ( + , ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
22 8 21 eqtr3id ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → Σ 𝑘𝐴 𝐵 = ( seq 1 ( + , ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
23 nnuz ℕ = ( ℤ ‘ 1 )
24 10 23 eleqtrdi ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ ‘ 1 ) )
25 fco ( ( ( 𝑘𝐴𝐵 ) : 𝐴𝑆𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ) → ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝑆 )
26 14 18 25 syl2anc ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝑆 )
27 26 ffvelrnda ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) ‘ 𝑥 ) ∈ 𝑆 )
28 2 adantlr ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
29 24 27 28 seqcl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → ( seq 1 ( + , ( ( 𝑘𝐴𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ∈ 𝑆 )
30 22 29 eqeltrd ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → Σ 𝑘𝐴 𝐵𝑆 )
31 30 expr ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 → Σ 𝑘𝐴 𝐵𝑆 ) )
32 31 exlimdv ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 → Σ 𝑘𝐴 𝐵𝑆 ) )
33 32 expimpd ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) → Σ 𝑘𝐴 𝐵𝑆 ) )
34 fz1f1o ( 𝐴 ∈ Fin → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) )
35 3 34 syl ( 𝜑 → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) )
36 7 33 35 mpjaod ( 𝜑 → Σ 𝑘𝐴 𝐵𝑆 )