This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 )