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	$⊢ φ \to O \in V$
	indsumin.2	$⊢ φ \to A \in Fin$
	indsumin.3	$⊢ φ \to A \subseteq O$
	indsumin.4	$⊢ φ \to B \subseteq O$
	indsumin.5	$⊢ (φ \land k \in A) \to C \in ℂ$
Assertion	indsumin	$⊢ φ \to \sum_{k \in A} 𝟙_{O} (B) (k) C = \sum_{k \in A \cap B} C$

Proof

Step	Hyp	Ref	Expression
1		indsumin.1	$⊢ φ \to O \in V$
2		indsumin.2	$⊢ φ \to A \in Fin$
3		indsumin.3	$⊢ φ \to A \subseteq O$
4		indsumin.4	$⊢ φ \to B \subseteq O$
5		indsumin.5	$⊢ (φ \land k \in A) \to C \in ℂ$
6		inindif	$⊢ (A \cap B) \cap (A ∖ B) = \emptyset$
7	6	a1i	$⊢ φ \to (A \cap B) \cap (A ∖ B) = \emptyset$
8		inundif	$⊢ (A \cap B) \cup (A ∖ B) = A$
9	8	eqcomi	$⊢ A = (A \cap B) \cup (A ∖ B)$
10	9	a1i	$⊢ φ \to A = (A \cap B) \cup (A ∖ B)$
11		pr01ssre	$⊢ \{0, 1\} \subseteq ℝ$
12		ax-resscn	$⊢ ℝ \subseteq ℂ$
13	11 12	sstri	$⊢ \{0, 1\} \subseteq ℂ$
14		indf	$⊢ (O \in V \land B \subseteq O) \to 𝟙_{O} (B) : O ⟶ \{0, 1\}$
15	1 4 14	syl2anc	$⊢ φ \to 𝟙_{O} (B) : O ⟶ \{0, 1\}$
16	15	adantr	$⊢ (φ \land k \in A) \to 𝟙_{O} (B) : O ⟶ \{0, 1\}$
17	3	sselda	$⊢ (φ \land k \in A) \to k \in O$
18	16 17	ffvelcdmd	$⊢ (φ \land k \in A) \to 𝟙_{O} (B) (k) \in \{0, 1\}$
19	13 18	sselid	$⊢ (φ \land k \in A) \to 𝟙_{O} (B) (k) \in ℂ$
20	19 5	mulcld	$⊢ (φ \land k \in A) \to 𝟙_{O} (B) (k) C \in ℂ$
21	7 10 2 20	fsumsplit	$⊢ φ \to \sum_{k \in A} 𝟙_{O} (B) (k) C = \sum_{k \in A \cap B} 𝟙_{O} (B) (k) C + \sum_{k \in A ∖ B} 𝟙_{O} (B) (k) C$
22	1	adantr	$⊢ (φ \land k \in (A \cap B)) \to O \in V$
23	4	adantr	$⊢ (φ \land k \in (A \cap B)) \to B \subseteq O$
24		inss2	$⊢ A \cap B \subseteq B$
25	24	a1i	$⊢ φ \to A \cap B \subseteq B$
26	25	sselda	$⊢ (φ \land k \in (A \cap B)) \to k \in B$
27		ind1	$⊢ (O \in V \land B \subseteq O \land k \in B) \to 𝟙_{O} (B) (k) = 1$
28	22 23 26 27	syl3anc	$⊢ (φ \land k \in (A \cap B)) \to 𝟙_{O} (B) (k) = 1$
29	28	oveq1d	$⊢ (φ \land k \in (A \cap B)) \to 𝟙_{O} (B) (k) C = 1 C$
30		inss1	$⊢ A \cap B \subseteq A$
31	30	a1i	$⊢ φ \to A \cap B \subseteq A$
32	31	sselda	$⊢ (φ \land k \in (A \cap B)) \to k \in A$
33	32 5	syldan	$⊢ (φ \land k \in (A \cap B)) \to C \in ℂ$
34	33	mullidd	$⊢ (φ \land k \in (A \cap B)) \to 1 C = C$
35	29 34	eqtrd	$⊢ (φ \land k \in (A \cap B)) \to 𝟙_{O} (B) (k) C = C$
36	35	sumeq2dv	$⊢ φ \to \sum_{k \in A \cap B} 𝟙_{O} (B) (k) C = \sum_{k \in A \cap B} C$
37	1	adantr	$⊢ (φ \land k \in (A ∖ B)) \to O \in V$
38	4	adantr	$⊢ (φ \land k \in (A ∖ B)) \to B \subseteq O$
39	3	ssdifd	$⊢ φ \to A ∖ B \subseteq O ∖ B$
40	39	sselda	$⊢ (φ \land k \in (A ∖ B)) \to k \in (O ∖ B)$
41		ind0	$⊢ (O \in V \land B \subseteq O \land k \in (O ∖ B)) \to 𝟙_{O} (B) (k) = 0$
42	37 38 40 41	syl3anc	$⊢ (φ \land k \in (A ∖ B)) \to 𝟙_{O} (B) (k) = 0$
43	42	oveq1d	$⊢ (φ \land k \in (A ∖ B)) \to 𝟙_{O} (B) (k) C = 0 \cdot C$
44		difssd	$⊢ φ \to A ∖ B \subseteq A$
45	44	sselda	$⊢ (φ \land k \in (A ∖ B)) \to k \in A$
46	45 5	syldan	$⊢ (φ \land k \in (A ∖ B)) \to C \in ℂ$
47	46	mul02d	$⊢ (φ \land k \in (A ∖ B)) \to 0 \cdot C = 0$
48	43 47	eqtrd	$⊢ (φ \land k \in (A ∖ B)) \to 𝟙_{O} (B) (k) C = 0$
49	48	sumeq2dv	$⊢ φ \to \sum_{k \in A ∖ B} 𝟙_{O} (B) (k) C = \sum_{k \in A ∖ B} 0$
50		diffi	$⊢ A \in Fin \to A ∖ B \in Fin$
51	2 50	syl	$⊢ φ \to A ∖ B \in Fin$
52		sumz	$⊢ (A ∖ B \subseteq ℤ_{\geq 0} \lor A ∖ B \in Fin) \to \sum_{k \in A ∖ B} 0 = 0$
53	52	olcs	$⊢ A ∖ B \in Fin \to \sum_{k \in A ∖ B} 0 = 0$
54	51 53	syl	$⊢ φ \to \sum_{k \in A ∖ B} 0 = 0$
55	49 54	eqtrd	$⊢ φ \to \sum_{k \in A ∖ B} 𝟙_{O} (B) (k) C = 0$
56	36 55	oveq12d	$⊢ φ \to \sum_{k \in A \cap B} 𝟙_{O} (B) (k) C + \sum_{k \in A ∖ B} 𝟙_{O} (B) (k) C = \sum_{k \in A \cap B} C + 0$
57		infi	$⊢ A \in Fin \to A \cap B \in Fin$
58	2 57	syl	$⊢ φ \to A \cap B \in Fin$
59	58 33	fsumcl	$⊢ φ \to \sum_{k \in A \cap B} C \in ℂ$
60	59	addridd	$⊢ φ \to \sum_{k \in A \cap B} C + 0 = \sum_{k \in A \cap B} C$
61	21 56 60	3eqtrd	$⊢ φ \to \sum_{k \in A} 𝟙_{O} (B) (k) C = \sum_{k \in A \cap B} C$

Metamath Proof Explorer

Theorem indsumin

Proof