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	$⊢ φ \to O \in Fin$
	indsum.2	$⊢ φ \to A \subseteq O$
	indsum.3	$⊢ (φ \land x \in O) \to B \in ℂ$
Assertion	indsum	$⊢ φ \to \sum_{x \in O} 𝟙_{O} (A) (x) B = \sum_{x \in A} B$

Proof

Step	Hyp	Ref	Expression
1		indsum.1	$⊢ φ \to O \in Fin$
2		indsum.2	$⊢ φ \to A \subseteq O$
3		indsum.3	$⊢ (φ \land x \in O) \to B \in ℂ$
4	2	sselda	$⊢ (φ \land x \in A) \to x \in O$
5	1 2	jca	$⊢ φ \to (O \in Fin \land A \subseteq O)$
6		fvindre	$⊢ ((O \in Fin \land A \subseteq O) \land x \in O) \to 𝟙_{O} (A) (x) \in ℝ$
7	5 6	sylan	$⊢ (φ \land x \in O) \to 𝟙_{O} (A) (x) \in ℝ$
8	7	recnd	$⊢ (φ \land x \in O) \to 𝟙_{O} (A) (x) \in ℂ$
9	8 3	mulcld	$⊢ (φ \land x \in O) \to 𝟙_{O} (A) (x) B \in ℂ$
10	4 9	syldan	$⊢ (φ \land x \in A) \to 𝟙_{O} (A) (x) B \in ℂ$
11	1	adantr	$⊢ (φ \land x \in (O ∖ A)) \to O \in Fin$
12	2	adantr	$⊢ (φ \land x \in (O ∖ A)) \to A \subseteq O$
13		simpr	$⊢ (φ \land x \in (O ∖ A)) \to x \in (O ∖ A)$
14		ind0	$⊢ (O \in Fin \land A \subseteq O \land x \in (O ∖ A)) \to 𝟙_{O} (A) (x) = 0$
15	11 12 13 14	syl3anc	$⊢ (φ \land x \in (O ∖ A)) \to 𝟙_{O} (A) (x) = 0$
16	15	oveq1d	$⊢ (φ \land x \in (O ∖ A)) \to 𝟙_{O} (A) (x) B = 0 \cdot B$
17		difssd	$⊢ φ \to O ∖ A \subseteq O$
18	17	sselda	$⊢ (φ \land x \in (O ∖ A)) \to x \in O$
19	3	mul02d	$⊢ (φ \land x \in O) \to 0 \cdot B = 0$
20	18 19	syldan	$⊢ (φ \land x \in (O ∖ A)) \to 0 \cdot B = 0$
21	16 20	eqtrd	$⊢ (φ \land x \in (O ∖ A)) \to 𝟙_{O} (A) (x) B = 0$
22	2 10 21 1	fsumss	$⊢ φ \to \sum_{x \in A} 𝟙_{O} (A) (x) B = \sum_{x \in O} 𝟙_{O} (A) (x) B$
23	1	adantr	$⊢ (φ \land x \in A) \to O \in Fin$
24	2	adantr	$⊢ (φ \land x \in A) \to A \subseteq O$
25		simpr	$⊢ (φ \land x \in A) \to x \in A$
26		ind1	$⊢ (O \in Fin \land A \subseteq O \land x \in A) \to 𝟙_{O} (A) (x) = 1$
27	23 24 25 26	syl3anc	$⊢ (φ \land x \in A) \to 𝟙_{O} (A) (x) = 1$
28	27	oveq1d	$⊢ (φ \land x \in A) \to 𝟙_{O} (A) (x) B = 1 B$
29	3	mullidd	$⊢ (φ \land x \in O) \to 1 B = B$
30	4 29	syldan	$⊢ (φ \land x \in A) \to 1 B = B$
31	28 30	eqtrd	$⊢ (φ \land x \in A) \to 𝟙_{O} (A) (x) B = B$
32	31	sumeq2dv	$⊢ φ \to \sum_{x \in A} 𝟙_{O} (A) (x) B = \sum_{x \in A} B$
33	22 32	eqtr3d	$⊢ φ \to \sum_{x \in O} 𝟙_{O} (A) (x) B = \sum_{x \in A} B$

Metamath Proof Explorer

Theorem indsum

Proof