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	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ ( 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) ∨ 𝐵 ∈ Fin ) ) → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 ⊆ 𝐵 )
2		iftrue	⊢ ( 𝑚 ∈ 𝐴 → if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) = ⦋ 𝑚 / 𝑘 ⦌ 𝐶 )
3	2	adantl	⊢ ( ( ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ∧ 𝑚 ∈ 𝐴 ) → if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) = ⦋ 𝑚 / 𝑘 ⦌ 𝐶 )
4		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐶
5	4	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ ℂ
6		csbeq1a	⊢ ( 𝑘 = 𝑚 → 𝐶 = ⦋ 𝑚 / 𝑘 ⦌ 𝐶 )
7	6	eleq1d	⊢ ( 𝑘 = 𝑚 → ( 𝐶 ∈ ℂ ↔ ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ ℂ ) )
8	5 7	rspc	⊢ ( 𝑚 ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ → ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ ℂ ) )
9	8	impcom	⊢ ( ( ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ∧ 𝑚 ∈ 𝐴 ) → ⦋ 𝑚 / 𝑘 ⦌ 𝐶 ∈ ℂ )
10	3 9	eqeltrd	⊢ ( ( ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ∧ 𝑚 ∈ 𝐴 ) → if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) ∈ ℂ )
11	10	ad4ant24	⊢ ( ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑚 ∈ 𝐴 ) → if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) ∈ ℂ )
12		eldifn	⊢ ( 𝑚 ∈ ( 𝐵 ∖ 𝐴 ) → ¬ 𝑚 ∈ 𝐴 )
13	12	iffalsed	⊢ ( 𝑚 ∈ ( 𝐵 ∖ 𝐴 ) → if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) = 0 )
14	13	adantl	⊢ ( ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑚 ∈ ( 𝐵 ∖ 𝐴 ) ) → if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) = 0 )
15		simpr	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) ) → 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) )
16	1 11 14 15	sumss	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) ) → Σ 𝑚 ∈ 𝐴 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) = Σ 𝑚 ∈ 𝐵 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) )
17		simpll	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ 𝐵 ∈ Fin ) → 𝐴 ⊆ 𝐵 )
18	10	ad4ant24	⊢ ( ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ 𝐵 ∈ Fin ) ∧ 𝑚 ∈ 𝐴 ) → if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) ∈ ℂ )
19	13	adantl	⊢ ( ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ 𝐵 ∈ Fin ) ∧ 𝑚 ∈ ( 𝐵 ∖ 𝐴 ) ) → if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) = 0 )
20		simpr	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ 𝐵 ∈ Fin ) → 𝐵 ∈ Fin )
21	17 18 19 20	fsumss	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ 𝐵 ∈ Fin ) → Σ 𝑚 ∈ 𝐴 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) = Σ 𝑚 ∈ 𝐵 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) )
22	16 21	jaodan	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ ( 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) ∨ 𝐵 ∈ Fin ) ) → Σ 𝑚 ∈ 𝐴 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) = Σ 𝑚 ∈ 𝐵 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) )
23		iftrue	⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = 𝐶 )
24	23	sumeq2i	⊢ Σ 𝑘 ∈ 𝐴 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = Σ 𝑘 ∈ 𝐴 𝐶
25		nfcv	⊢ Ⅎ 𝑚 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 )
26		nfv	⊢ Ⅎ 𝑘 𝑚 ∈ 𝐴
27		nfcv	⊢ Ⅎ 𝑘 0
28	26 4 27	nfif	⊢ Ⅎ 𝑘 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 )
29		eleq1w	⊢ ( 𝑘 = 𝑚 → ( 𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴 ) )
30	29 6	ifbieq1d	⊢ ( 𝑘 = 𝑚 → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) )
31	25 28 30	cbvsumi	⊢ Σ 𝑘 ∈ 𝐴 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = Σ 𝑚 ∈ 𝐴 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 )
32	24 31	eqtr3i	⊢ Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑚 ∈ 𝐴 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 )
33	25 28 30	cbvsumi	⊢ Σ 𝑘 ∈ 𝐵 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = Σ 𝑚 ∈ 𝐵 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 )
34	22 32 33	3eqtr4g	⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ ( 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) ∨ 𝐵 ∈ Fin ) ) → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) )