Metamath Proof Explorer

Theorem indsum

Description: Finite sum of a product with the indicator function / Cartesian product with the indicator function. (Contributed by Thierry Arnoux, 14-Aug-2017)

Ref Expression
Hypotheses indsum.1 ⊢ ( 𝜑 → 𝑂 ∈ Fin )
indsum.2 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑂 )
indsum.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → 𝐵 ∈ ℂ )
Assertion indsum ( 𝜑 → Σ 𝑥 ∈ 𝑂 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = Σ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 indsum.1 ⊢ ( 𝜑 → 𝑂 ∈ Fin )
2 indsum.2 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑂 )
3 indsum.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → 𝐵 ∈ ℂ )
4 2 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝑂 )
5 pr01ssre ⊢ { 0 , 1 } ⊆ ℝ
6 indf ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } )
7 1 2 6 syl2anc ⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } )
8 7 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) ∈ { 0 , 1 } )
9 5 8 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) ∈ ℝ )
10 9 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) ∈ ℂ )
11 10 3 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) ∈ ℂ )
12 4 11 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) ∈ ℂ )
13 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → 𝑂 ∈ Fin )
14 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → 𝐴 ⊆ 𝑂 )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) )
16 ind0 ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 0 )
17 13 14 15 16 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 0 )
18 17 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = ( 0 · 𝐵 ) )
19 difssd ⊢ ( 𝜑 → ( 𝑂 ∖ 𝐴 ) ⊆ 𝑂 )
20 19 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → 𝑥 ∈ 𝑂 )
21 3 mul02d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( 0 · 𝐵 ) = 0 )
22 20 21 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → ( 0 · 𝐵 ) = 0 )
23 18 22 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = 0 )
24 2 12 23 1 fsumss ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = Σ 𝑥 ∈ 𝑂 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) )
25 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑂 ∈ Fin )
26 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ 𝑂 )
27 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
28 ind1 ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 1 )
29 25 26 27 28 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 1 )
30 29 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = ( 1 · 𝐵 ) )
31 3 mulid2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( 1 · 𝐵 ) = 𝐵 )
32 4 31 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1 · 𝐵 ) = 𝐵 )
33 30 32 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = 𝐵 )
34 33 sumeq2dv ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = Σ 𝑥 ∈ 𝐴 𝐵 )
35 24 34 eqtr3d ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝑂 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = Σ 𝑥 ∈ 𝐴 𝐵 )