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

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 ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ ( 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) ∨ 𝐵 ∈ 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 eleq1w ⊢ ( 𝑘 = 𝑚 → ( 𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴 ) )
26 25 6 ifbieq1d ⊢ ( 𝑘 = 𝑚 → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 ) )
27 nfcv ⊢ Ⅎ 𝑚 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 )
28 nfv ⊢ Ⅎ 𝑘 𝑚 ∈ 𝐴
29 nfcv ⊢ Ⅎ 𝑘 0
30 28 4 29 nfif ⊢ Ⅎ 𝑘 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 )
31 26 27 30 cbvsum ⊢ Σ 𝑘 ∈ 𝐴 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = Σ 𝑚 ∈ 𝐴 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 )
32 24 31 eqtr3i ⊢ Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑚 ∈ 𝐴 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 )
33 26 27 30 cbvsum ⊢ Σ 𝑘 ∈ 𝐵 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = Σ 𝑚 ∈ 𝐵 if ( 𝑚 ∈ 𝐴 , ⦋ 𝑚 / 𝑘 ⦌ 𝐶 , 0 )
34 22 32 33 3eqtr4g ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 𝐶 ∈ ℂ ) ∧ ( 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) ∨ 𝐵 ∈ Fin ) ) → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) )