Metamath Proof Explorer

Theorem sumss2

Description: Change the index set of a sum by adding zeroes. (Contributed by Mario Carneiro, 15-Jul-2013) (Revised by Mario Carneiro, 20-Apr-2014)

Ref Expression
Assertion sumss2 ⊢A⊆B∧∀k∈AC∈ℂ∧B⊆ℤ≥M∨B∈Fin→∑k∈AC=∑k∈Bifk∈AC0

Proof

Step Hyp Ref Expression
1 simpll ⊢A⊆B∧∀k∈AC∈ℂ∧B⊆ℤ≥M→A⊆B
2 iftrue ⊢m∈A→ifm∈A⦋m/k⦌C0=⦋m/k⦌C
3 2 adantl ⊢∀k∈AC∈ℂ∧m∈A→ifm∈A⦋m/k⦌C0=⦋m/k⦌C
4 nfcsb1v ⊢Ⅎ_k⦋m/k⦌C
5 4 nfel1 ⊢Ⅎk⦋m/k⦌C∈ℂ
6 csbeq1a ⊢k=m→C=⦋m/k⦌C
7 6 eleq1d ⊢k=m→C∈ℂ↔⦋m/k⦌C∈ℂ
8 5 7 rspc ⊢m∈A→∀k∈AC∈ℂ→⦋m/k⦌C∈ℂ
9 8 impcom ⊢∀k∈AC∈ℂ∧m∈A→⦋m/k⦌C∈ℂ
10 3 9 eqeltrd ⊢∀k∈AC∈ℂ∧m∈A→ifm∈A⦋m/k⦌C0∈ℂ
11 10 ad4ant24 ⊢A⊆B∧∀k∈AC∈ℂ∧B⊆ℤ≥M∧m∈A→ifm∈A⦋m/k⦌C0∈ℂ
12 eldifn ⊢m∈B∖A→¬m∈A
13 12 iffalsed ⊢m∈B∖A→ifm∈A⦋m/k⦌C0=0
14 13 adantl ⊢A⊆B∧∀k∈AC∈ℂ∧B⊆ℤ≥M∧m∈B∖A→ifm∈A⦋m/k⦌C0=0
15 simpr ⊢A⊆B∧∀k∈AC∈ℂ∧B⊆ℤ≥M→B⊆ℤ≥M
16 1 11 14 15 sumss ⊢A⊆B∧∀k∈AC∈ℂ∧B⊆ℤ≥M→∑m∈Aifm∈A⦋m/k⦌C0=∑m∈Bifm∈A⦋m/k⦌C0
17 simpll ⊢A⊆B∧∀k∈AC∈ℂ∧B∈Fin→A⊆B
18 10 ad4ant24 ⊢A⊆B∧∀k∈AC∈ℂ∧B∈Fin∧m∈A→ifm∈A⦋m/k⦌C0∈ℂ
19 13 adantl ⊢A⊆B∧∀k∈AC∈ℂ∧B∈Fin∧m∈B∖A→ifm∈A⦋m/k⦌C0=0
20 simpr ⊢A⊆B∧∀k∈AC∈ℂ∧B∈Fin→B∈Fin
21 17 18 19 20 fsumss ⊢A⊆B∧∀k∈AC∈ℂ∧B∈Fin→∑m∈Aifm∈A⦋m/k⦌C0=∑m∈Bifm∈A⦋m/k⦌C0
22 16 21 jaodan ⊢A⊆B∧∀k∈AC∈ℂ∧B⊆ℤ≥M∨B∈Fin→∑m∈Aifm∈A⦋m/k⦌C0=∑m∈Bifm∈A⦋m/k⦌C0
23 iftrue ⊢k∈A→ifk∈AC0=C
24 23 sumeq2i ⊢∑k∈Aifk∈AC0=∑k∈AC
25 nfcv ⊢Ⅎ_mifk∈AC0
26 nfv ⊢Ⅎkm∈A
27 nfcv ⊢Ⅎ_k0
28 26 4 27 nfif ⊢Ⅎ_kifm∈A⦋m/k⦌C0
29 eleq1w ⊢k=m→k∈A↔m∈A
30 29 6 ifbieq1d ⊢k=m→ifk∈AC0=ifm∈A⦋m/k⦌C0
31 25 28 30 cbvsumi ⊢∑k∈Aifk∈AC0=∑m∈Aifm∈A⦋m/k⦌C0
32 24 31 eqtr3i ⊢∑k∈AC=∑m∈Aifm∈A⦋m/k⦌C0
33 25 28 30 cbvsumi ⊢∑k∈Bifk∈AC0=∑m∈Bifm∈A⦋m/k⦌C0
34 22 32 33 3eqtr4g ⊢A⊆B∧∀k∈AC∈ℂ∧B⊆ℤ≥M∨B∈Fin→∑k∈AC=∑k∈Bifk∈AC0