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 ⊢ φ → S ⊆ ℂ
fsumcllem.2 ⊢ φ ∧ x ∈ S ∧ y ∈ S → x + y ∈ S
fsumcllem.3 ⊢ φ → A ∈ Fin
fsumcllem.4 ⊢ φ ∧ k ∈ A → B ∈ S
fsumcllem.5 ⊢ φ → 0 ∈ S
Assertion fsumcllem ⊢ φ → ∑ k ∈ A B ∈ S

Proof

Step Hyp Ref Expression
1 fsumcllem.1 ⊢ φ → S ⊆ ℂ
2 fsumcllem.2 ⊢ φ ∧ x ∈ S ∧ y ∈ S → x + y ∈ S
3 fsumcllem.3 ⊢ φ → A ∈ Fin
4 fsumcllem.4 ⊢ φ ∧ k ∈ A → B ∈ S
5 fsumcllem.5 ⊢ φ → 0 ∈ S
6 simpr ⊢ φ ∧ A = ∅ → A = ∅
7 6 sumeq1d ⊢ φ ∧ A = ∅ → ∑ k ∈ A B = ∑ k ∈ ∅ B
8 sum0 ⊢ ∑ k ∈ ∅ B = 0
9 7 8 eqtrdi ⊢ φ ∧ A = ∅ → ∑ k ∈ A B = 0
10 5 adantr ⊢ φ ∧ A = ∅ → 0 ∈ S
11 9 10 eqeltrd ⊢ φ ∧ A = ∅ → ∑ k ∈ A B ∈ S
12 1 adantr ⊢ φ ∧ A ≠ ∅ → S ⊆ ℂ
13 2 adantlr ⊢ φ ∧ A ≠ ∅ ∧ x ∈ S ∧ y ∈ S → x + y ∈ S
14 3 adantr ⊢ φ ∧ A ≠ ∅ → A ∈ Fin
15 4 adantlr ⊢ φ ∧ A ≠ ∅ ∧ k ∈ A → B ∈ S
16 simpr ⊢ φ ∧ A ≠ ∅ → A ≠ ∅
17 12 13 14 15 16 fsumcl2lem ⊢ φ ∧ A ≠ ∅ → ∑ k ∈ A B ∈ S
18 11 17 pm2.61dane ⊢ φ → ∑ k ∈ A B ∈ S