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 ⊢ φ → O ∈ Fin
indsum.2 ⊢ φ → A ⊆ O
indsum.3 ⊢ φ ∧ x ∈ O → B ∈ ℂ
Assertion indsum ⊢ φ → ∑ x ∈ O 𝟙 O ⁡ A ⁡ x ⁢ B = ∑ x ∈ A B

Proof

Step Hyp Ref Expression
1 indsum.1 ⊢ φ → O ∈ Fin
2 indsum.2 ⊢ φ → A ⊆ O
3 indsum.3 ⊢ φ ∧ x ∈ O → B ∈ ℂ
4 2 sselda ⊢ φ ∧ x ∈ A → x ∈ O
5 pr01ssre ⊢ 0 1 ⊆ ℝ
6 indf ⊢ O ∈ Fin ∧ A ⊆ O → 𝟙 O ⁡ A : O ⟶ 0 1
7 1 2 6 syl2anc ⊢ φ → 𝟙 O ⁡ A : O ⟶ 0 1
8 7 ffvelrnda ⊢ φ ∧ x ∈ O → 𝟙 O ⁡ A ⁡ x ∈ 0 1
9 5 8 sselid ⊢ φ ∧ x ∈ O → 𝟙 O ⁡ A ⁡ x ∈ ℝ
10 9 recnd ⊢ φ ∧ x ∈ O → 𝟙 O ⁡ A ⁡ x ∈ ℂ
11 10 3 mulcld ⊢ φ ∧ x ∈ O → 𝟙 O ⁡ A ⁡ x ⁢ B ∈ ℂ
12 4 11 syldan ⊢ φ ∧ x ∈ A → 𝟙 O ⁡ A ⁡ x ⁢ B ∈ ℂ
13 1 adantr ⊢ φ ∧ x ∈ O ∖ A → O ∈ Fin
14 2 adantr ⊢ φ ∧ x ∈ O ∖ A → A ⊆ O
15 simpr ⊢ φ ∧ x ∈ O ∖ A → x ∈ O ∖ A
16 ind0 ⊢ O ∈ Fin ∧ A ⊆ O ∧ x ∈ O ∖ A → 𝟙 O ⁡ A ⁡ x = 0
17 13 14 15 16 syl3anc ⊢ φ ∧ x ∈ O ∖ A → 𝟙 O ⁡ A ⁡ x = 0
18 17 oveq1d ⊢ φ ∧ x ∈ O ∖ A → 𝟙 O ⁡ A ⁡ x ⁢ B = 0 ⋅ B
19 difssd ⊢ φ → O ∖ A ⊆ O
20 19 sselda ⊢ φ ∧ x ∈ O ∖ A → x ∈ O
21 3 mul02d ⊢ φ ∧ x ∈ O → 0 ⋅ B = 0
22 20 21 syldan ⊢ φ ∧ x ∈ O ∖ A → 0 ⋅ B = 0
23 18 22 eqtrd ⊢ φ ∧ x ∈ O ∖ A → 𝟙 O ⁡ A ⁡ x ⁢ B = 0
24 2 12 23 1 fsumss ⊢ φ → ∑ x ∈ A 𝟙 O ⁡ A ⁡ x ⁢ B = ∑ x ∈ O 𝟙 O ⁡ A ⁡ x ⁢ B
25 1 adantr ⊢ φ ∧ x ∈ A → O ∈ Fin
26 2 adantr ⊢ φ ∧ x ∈ A → A ⊆ O
27 simpr ⊢ φ ∧ x ∈ A → x ∈ A
28 ind1 ⊢ O ∈ Fin ∧ A ⊆ O ∧ x ∈ A → 𝟙 O ⁡ A ⁡ x = 1
29 25 26 27 28 syl3anc ⊢ φ ∧ x ∈ A → 𝟙 O ⁡ A ⁡ x = 1
30 29 oveq1d ⊢ φ ∧ x ∈ A → 𝟙 O ⁡ A ⁡ x ⁢ B = 1 ⁢ B
31 3 mulid2d ⊢ φ ∧ x ∈ O → 1 ⁢ B = B
32 4 31 syldan ⊢ φ ∧ x ∈ A → 1 ⁢ B = B
33 30 32 eqtrd ⊢ φ ∧ x ∈ A → 𝟙 O ⁡ A ⁡ x ⁢ B = B
34 33 sumeq2dv ⊢ φ → ∑ x ∈ A 𝟙 O ⁡ A ⁡ x ⁢ B = ∑ x ∈ A B
35 24 34 eqtr3d ⊢ φ → ∑ x ∈ O 𝟙 O ⁡ A ⁡ x ⁢ B = ∑ x ∈ A B