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

Metamath Proof Explorer

Theorem indsumin

Description: Finite sum of a product with the indicator function / Cartesian product with the indicator function. (Contributed by Thierry Arnoux, 11-Dec-2021)

Ref Expression
Hypotheses indsumin.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
indsumin.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
indsumin.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑂 )
indsumin.4 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑂 )
indsumin.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
Assertion indsumin ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 )

Proof

Step Hyp Ref Expression
1 indsumin.1 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2 indsumin.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
3 indsumin.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑂 )
4 indsumin.4 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑂 )
5 indsumin.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
6 inindif ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅
7 6 a1i ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅ )
8 inundif ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴
9 8 eqcomi ⊢ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) )
10 9 a1i ⊢ ( 𝜑 → 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) )
11 pr01ssre ⊢ { 0 , 1 } ⊆ ℝ
12 ax-resscn ⊢ ℝ ⊆ ℂ
13 11 12 sstri ⊢ { 0 , 1 } ⊆ ℂ
14 indf ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐵 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) : 𝑂 ⟶ { 0 , 1 } )
15 1 4 14 syl2anc ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) : 𝑂 ⟶ { 0 , 1 } )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) : 𝑂 ⟶ { 0 , 1 } )
17 3 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝑂 )
18 16 17 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) ∈ { 0 , 1 } )
19 13 18 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℂ )
20 19 5 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) ∈ ℂ )
21 7 10 2 20 fsumsplit ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = ( Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) + Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) ) )
22 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑂 ∈ 𝑉 )
23 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐵 ⊆ 𝑂 )
24 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
25 24 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 )
26 25 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑘 ∈ 𝐵 )
27 ind1 ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐵 ⊆ 𝑂 ∧ 𝑘 ∈ 𝐵 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) = 1 )
28 22 23 26 27 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) = 1 )
29 28 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = ( 1 · 𝐶 ) )
30 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
31 30 a1i ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 )
32 31 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑘 ∈ 𝐴 )
33 32 5 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐶 ∈ ℂ )
34 33 mullidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( 1 · 𝐶 ) = 𝐶 )
35 29 34 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = 𝐶 )
36 35 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 )
37 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝑂 ∈ 𝑉 )
38 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝐵 ⊆ 𝑂 )
39 3 ssdifd ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ ( 𝑂 ∖ 𝐵 ) )
40 39 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝑘 ∈ ( 𝑂 ∖ 𝐵 ) )
41 ind0 ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐵 ⊆ 𝑂 ∧ 𝑘 ∈ ( 𝑂 ∖ 𝐵 ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) = 0 )
42 37 38 40 41 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) = 0 )
43 42 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = ( 0 · 𝐶 ) )
44 difssd ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 )
45 44 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝑘 ∈ 𝐴 )
46 45 5 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝐶 ∈ ℂ )
47 46 mul02d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → ( 0 · 𝐶 ) = 0 )
48 43 47 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = 0 )
49 48 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 0 )
50 diffi ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ 𝐵 ) ∈ Fin )
51 2 50 syl ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ∈ Fin )
52 sumz ⊢ ( ( ( 𝐴 ∖ 𝐵 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 𝐴 ∖ 𝐵 ) ∈ Fin ) → Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 0 = 0 )
53 52 olcs ⊢ ( ( 𝐴 ∖ 𝐵 ) ∈ Fin → Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 0 = 0 )
54 51 53 syl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 0 = 0 )
55 49 54 eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = 0 )
56 36 55 oveq12d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) + Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) ) = ( Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 + 0 ) )
57 infi ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∩ 𝐵 ) ∈ Fin )
58 2 57 syl ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ Fin )
59 58 33 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 ∈ ℂ )
60 59 addridd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 + 0 ) = Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 )
61 21 56 60 3eqtrd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 )