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 ∈ A C ∈ ℂ ∧ B ⊆ ℤ ≥ M ∨ B ∈ Fin → ∑ k ∈ A C = ∑ k ∈ B if k ∈ A C 0

Proof

Step Hyp Ref Expression
1 simpll ⊢ A ⊆ B ∧ ∀ k ∈ A C ∈ ℂ ∧ B ⊆ ℤ ≥ M → A ⊆ B
2 iftrue ⊢ m ∈ A → if m ∈ A ⦋ m / k⦌ C 0 = ⦋ m / k⦌ C
3 2 adantl ⊢ ∀ k ∈ A C ∈ ℂ ∧ m ∈ A → if m ∈ A ⦋ m / k⦌ C 0 = ⦋ 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 ∈ A C ∈ ℂ → ⦋ m / k⦌ C ∈ ℂ
9 8 impcom ⊢ ∀ k ∈ A C ∈ ℂ ∧ m ∈ A → ⦋ m / k⦌ C ∈ ℂ
10 3 9 eqeltrd ⊢ ∀ k ∈ A C ∈ ℂ ∧ m ∈ A → if m ∈ A ⦋ m / k⦌ C 0 ∈ ℂ
11 10 ad4ant24 ⊢ A ⊆ B ∧ ∀ k ∈ A C ∈ ℂ ∧ B ⊆ ℤ ≥ M ∧ m ∈ A → if m ∈ A ⦋ m / k⦌ C 0 ∈ ℂ
12 eldifn ⊢ m ∈ B ∖ A → ¬ m ∈ A
13 12 iffalsed ⊢ m ∈ B ∖ A → if m ∈ A ⦋ m / k⦌ C 0 = 0
14 13 adantl ⊢ A ⊆ B ∧ ∀ k ∈ A C ∈ ℂ ∧ B ⊆ ℤ ≥ M ∧ m ∈ B ∖ A → if m ∈ A ⦋ m / k⦌ C 0 = 0
15 simpr ⊢ A ⊆ B ∧ ∀ k ∈ A C ∈ ℂ ∧ B ⊆ ℤ ≥ M → B ⊆ ℤ ≥ M
16 1 11 14 15 sumss ⊢ A ⊆ B ∧ ∀ k ∈ A C ∈ ℂ ∧ B ⊆ ℤ ≥ M → ∑ m ∈ A if m ∈ A ⦋ m / k⦌ C 0 = ∑ m ∈ B if m ∈ A ⦋ m / k⦌ C 0
17 simpll ⊢ A ⊆ B ∧ ∀ k ∈ A C ∈ ℂ ∧ B ∈ Fin → A ⊆ B
18 10 ad4ant24 ⊢ A ⊆ B ∧ ∀ k ∈ A C ∈ ℂ ∧ B ∈ Fin ∧ m ∈ A → if m ∈ A ⦋ m / k⦌ C 0 ∈ ℂ
19 13 adantl ⊢ A ⊆ B ∧ ∀ k ∈ A C ∈ ℂ ∧ B ∈ Fin ∧ m ∈ B ∖ A → if m ∈ A ⦋ m / k⦌ C 0 = 0
20 simpr ⊢ A ⊆ B ∧ ∀ k ∈ A C ∈ ℂ ∧ B ∈ Fin → B ∈ Fin
21 17 18 19 20 fsumss ⊢ A ⊆ B ∧ ∀ k ∈ A C ∈ ℂ ∧ B ∈ Fin → ∑ m ∈ A if m ∈ A ⦋ m / k⦌ C 0 = ∑ m ∈ B if m ∈ A ⦋ m / k⦌ C 0
22 16 21 jaodan ⊢ A ⊆ B ∧ ∀ k ∈ A C ∈ ℂ ∧ B ⊆ ℤ ≥ M ∨ B ∈ Fin → ∑ m ∈ A if m ∈ A ⦋ m / k⦌ C 0 = ∑ m ∈ B if m ∈ A ⦋ m / k⦌ C 0
23 iftrue ⊢ k ∈ A → if k ∈ A C 0 = C
24 23 sumeq2i ⊢ ∑ k ∈ A if k ∈ A C 0 = ∑ k ∈ A C
25 eleq1w ⊢ k = m → k ∈ A ↔ m ∈ A
26 25 6 ifbieq1d ⊢ k = m → if k ∈ A C 0 = if m ∈ A ⦋ m / k⦌ C 0
27 nfcv ⊢ Ⅎ _ m if k ∈ A C 0
28 nfv ⊢ Ⅎ k m ∈ A
29 nfcv ⊢ Ⅎ _ k 0
30 28 4 29 nfif ⊢ Ⅎ _ k if m ∈ A ⦋ m / k⦌ C 0
31 26 27 30 cbvsum ⊢ ∑ k ∈ A if k ∈ A C 0 = ∑ m ∈ A if m ∈ A ⦋ m / k⦌ C 0
32 24 31 eqtr3i ⊢ ∑ k ∈ A C = ∑ m ∈ A if m ∈ A ⦋ m / k⦌ C 0
33 26 27 30 cbvsum ⊢ ∑ k ∈ B if k ∈ A C 0 = ∑ m ∈ B if m ∈ A ⦋ m / k⦌ C 0
34 22 32 33 3eqtr4g ⊢ A ⊆ B ∧ ∀ k ∈ A C ∈ ℂ ∧ B ⊆ ℤ ≥ M ∨ B ∈ Fin → ∑ k ∈ A C = ∑ k ∈ B if k ∈ A C 0