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

Metamath Proof Explorer

Theorem indsum

Description: Finite sum of a product with the indicator function / Cartesian product with the indicator function. Note: this theorem cannot be efficiently shortened using sumss2 , unless there are some additional auxiliary theorems like ( if ( x e. A , 1 , 0 ) x. B ) = if ( x e. A , B , 0 ) . (Contributed by Thierry Arnoux, 14-Aug-2017) (Proof shortened by AV, 11-Apr-2026)

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 1 2 jca ⊢ ( 𝜑 → ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) )
6 fvindre ⊢ ( ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) ∧ 𝑥 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) ∈ ℝ )
7 5 6 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) ∈ ℝ )
8 7 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) ∈ ℂ )
9 8 3 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) ∈ ℂ )
10 4 9 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) ∈ ℂ )
11 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → 𝑂 ∈ Fin )
12 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → 𝐴 ⊆ 𝑂 )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) )
14 ind0 ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 0 )
15 11 12 13 14 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 0 )
16 15 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = ( 0 · 𝐵 ) )
17 difssd ⊢ ( 𝜑 → ( 𝑂 ∖ 𝐴 ) ⊆ 𝑂 )
18 17 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → 𝑥 ∈ 𝑂 )
19 3 mul02d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( 0 · 𝐵 ) = 0 )
20 18 19 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → ( 0 · 𝐵 ) = 0 )
21 16 20 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑂 ∖ 𝐴 ) ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = 0 )
22 2 10 21 1 fsumss ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = Σ 𝑥 ∈ 𝑂 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) )
23 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑂 ∈ Fin )
24 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ 𝑂 )
25 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
26 ind1 ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 1 )
27 23 24 25 26 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) = 1 )
28 27 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = ( 1 · 𝐵 ) )
29 3 mullidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑂 ) → ( 1 · 𝐵 ) = 𝐵 )
30 4 29 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1 · 𝐵 ) = 𝐵 )
31 28 30 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = 𝐵 )
32 31 sumeq2dv ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = Σ 𝑥 ∈ 𝐴 𝐵 )
33 22 32 eqtr3d ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝑂 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑥 ) · 𝐵 ) = Σ 𝑥 ∈ 𝐴 𝐵 )