Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 fsumcllem.1 ( 𝜑𝑆 ⊆ ℂ )
2 fsumcllem.2 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
3 fsumcllem.3 ( 𝜑𝐴 ∈ Fin )
4 fsumcllem.4 ( ( 𝜑𝑘𝐴 ) → 𝐵𝑆 )
5 fsumcllem.5 ( 𝜑 → 0 ∈ 𝑆 )
6 simpr ( ( 𝜑𝐴 = ∅ ) → 𝐴 = ∅ )
7 6 sumeq1d ( ( 𝜑𝐴 = ∅ ) → Σ 𝑘𝐴 𝐵 = Σ 𝑘 ∈ ∅ 𝐵 )
8 sum0 Σ 𝑘 ∈ ∅ 𝐵 = 0
9 7 8 eqtrdi ( ( 𝜑𝐴 = ∅ ) → Σ 𝑘𝐴 𝐵 = 0 )
10 5 adantr ( ( 𝜑𝐴 = ∅ ) → 0 ∈ 𝑆 )
11 9 10 eqeltrd ( ( 𝜑𝐴 = ∅ ) → Σ 𝑘𝐴 𝐵𝑆 )
12 1 adantr ( ( 𝜑𝐴 ≠ ∅ ) → 𝑆 ⊆ ℂ )
13 2 adantlr ( ( ( 𝜑𝐴 ≠ ∅ ) ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
14 3 adantr ( ( 𝜑𝐴 ≠ ∅ ) → 𝐴 ∈ Fin )
15 4 adantlr ( ( ( 𝜑𝐴 ≠ ∅ ) ∧ 𝑘𝐴 ) → 𝐵𝑆 )
16 simpr ( ( 𝜑𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
17 12 13 14 15 16 fsumcl2lem ( ( 𝜑𝐴 ≠ ∅ ) → Σ 𝑘𝐴 𝐵𝑆 )
18 11 17 pm2.61dane ( 𝜑 → Σ 𝑘𝐴 𝐵𝑆 )