Theorem 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	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
	indsumin.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	indsumin.3	⊢ ( 𝜑 → 𝐴 ⊆ 𝑂 )
	indsumin.4	⊢ ( 𝜑 → 𝐵 ⊆ 𝑂 )
	indsumin.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
Assertion	indsumin	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		indsumin.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2		indsumin.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		indsumin.3	⊢ ( 𝜑 → 𝐴 ⊆ 𝑂 )
4		indsumin.4	⊢ ( 𝜑 → 𝐵 ⊆ 𝑂 )
5		indsumin.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
6		inindif	⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅
7	6	a1i	⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ∩ ( 𝐴 ∖ 𝐵 ) ) = ∅ )
8		inundif	⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴
9	8	eqcomi	⊢ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) )
10	9	a1i	⊢ ( 𝜑 → 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) )
11		pr01ssre	⊢ { 0 , 1 } ⊆ ℝ
12		ax-resscn	⊢ ℝ ⊆ ℂ
13	11 12	sstri	⊢ { 0 , 1 } ⊆ ℂ
14		indf	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐵 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) : 𝑂 ⟶ { 0 , 1 } )
15	1 4 14	syl2anc	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) : 𝑂 ⟶ { 0 , 1 } )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) : 𝑂 ⟶ { 0 , 1 } )
17	3	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝑂 )
18	16 17	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) ∈ { 0 , 1 } )
19	13 18	sselid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) ∈ ℂ )
20	19 5	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) ∈ ℂ )
21	7 10 2 20	fsumsplit	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = ( Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) + Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) ) )
22	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑂 ∈ 𝑉 )
23	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐵 ⊆ 𝑂 )
24		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
25	24	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 )
26	25	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑘 ∈ 𝐵 )
27		ind1	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐵 ⊆ 𝑂 ∧ 𝑘 ∈ 𝐵 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) = 1 )
28	22 23 26 27	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) = 1 )
29	28	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = ( 1 · 𝐶 ) )
30		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
31	30	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 )
32	31	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑘 ∈ 𝐴 )
33	32 5	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐶 ∈ ℂ )
34	33	mulid2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( 1 · 𝐶 ) = 𝐶 )
35	29 34	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = 𝐶 )
36	35	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 )
37	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝑂 ∈ 𝑉 )
38	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝐵 ⊆ 𝑂 )
39	3	ssdifd	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ ( 𝑂 ∖ 𝐵 ) )
40	39	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝑘 ∈ ( 𝑂 ∖ 𝐵 ) )
41		ind0	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐵 ⊆ 𝑂 ∧ 𝑘 ∈ ( 𝑂 ∖ 𝐵 ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) = 0 )
42	37 38 40 41	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) = 0 )
43	42	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = ( 0 · 𝐶 ) )
44		difssd	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 )
45	44	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝑘 ∈ 𝐴 )
46	45 5	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → 𝐶 ∈ ℂ )
47	46	mul02d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → ( 0 · 𝐶 ) = 0 )
48	43 47	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = 0 )
49	48	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 0 )
50		diffi	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ 𝐵 ) ∈ Fin )
51	2 50	syl	⊢ ( 𝜑 → ( 𝐴 ∖ 𝐵 ) ∈ Fin )
52		sumz	⊢ ( ( ( 𝐴 ∖ 𝐵 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 𝐴 ∖ 𝐵 ) ∈ Fin ) → Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 0 = 0 )
53	52	olcs	⊢ ( ( 𝐴 ∖ 𝐵 ) ∈ Fin → Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 0 = 0 )
54	51 53	syl	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) 0 = 0 )
55	49 54	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = 0 )
56	36 55	oveq12d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) + Σ 𝑘 ∈ ( 𝐴 ∖ 𝐵 ) ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) ) = ( Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 + 0 ) )
57		infi	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∩ 𝐵 ) ∈ Fin )
58	2 57	syl	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ Fin )
59	58 33	fsumcl	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 ∈ ℂ )
60	59	addid1d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 + 0 ) = Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 )
61	21 56 60	3eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐵 ) ‘ 𝑘 ) · 𝐶 ) = Σ 𝑘 ∈ ( 𝐴 ∩ 𝐵 ) 𝐶 )