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	|- ( ph -> O e. Fin )
	indsum.2	|- ( ph -> A C_ O )
	indsum.3	|- ( ( ph /\ x e. O ) -> B e. CC )
Assertion	indsum	|- ( ph -> sum_ x e. O ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = sum_ x e. A B )

Proof

Step	Hyp	Ref	Expression
1		indsum.1	|- ( ph -> O e. Fin )
2		indsum.2	|- ( ph -> A C_ O )
3		indsum.3	|- ( ( ph /\ x e. O ) -> B e. CC )
4	2	sselda	|- ( ( ph /\ x e. A ) -> x e. O )
5	1 2	jca	|- ( ph -> ( O e. Fin /\ A C_ O ) )
6		fvindre	|- ( ( ( O e. Fin /\ A C_ O ) /\ x e. O ) -> ( ( ( _Ind ` O ) ` A ) ` x ) e. RR )
7	5 6	sylan	|- ( ( ph /\ x e. O ) -> ( ( ( _Ind ` O ) ` A ) ` x ) e. RR )
8	7	recnd	|- ( ( ph /\ x e. O ) -> ( ( ( _Ind ` O ) ` A ) ` x ) e. CC )
9	8 3	mulcld	|- ( ( ph /\ x e. O ) -> ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) e. CC )
10	4 9	syldan	|- ( ( ph /\ x e. A ) -> ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) e. CC )
11	1	adantr	|- ( ( ph /\ x e. ( O \ A ) ) -> O e. Fin )
12	2	adantr	|- ( ( ph /\ x e. ( O \ A ) ) -> A C_ O )
13		simpr	|- ( ( ph /\ x e. ( O \ A ) ) -> x e. ( O \ A ) )
14		ind0	|- ( ( O e. Fin /\ A C_ O /\ x e. ( O \ A ) ) -> ( ( ( _Ind ` O ) ` A ) ` x ) = 0 )
15	11 12 13 14	syl3anc	|- ( ( ph /\ x e. ( O \ A ) ) -> ( ( ( _Ind ` O ) ` A ) ` x ) = 0 )
16	15	oveq1d	|- ( ( ph /\ x e. ( O \ A ) ) -> ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = ( 0 x. B ) )
17		difssd	|- ( ph -> ( O \ A ) C_ O )
18	17	sselda	|- ( ( ph /\ x e. ( O \ A ) ) -> x e. O )
19	3	mul02d	|- ( ( ph /\ x e. O ) -> ( 0 x. B ) = 0 )
20	18 19	syldan	|- ( ( ph /\ x e. ( O \ A ) ) -> ( 0 x. B ) = 0 )
21	16 20	eqtrd	|- ( ( ph /\ x e. ( O \ A ) ) -> ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = 0 )
22	2 10 21 1	fsumss	|- ( ph -> sum_ x e. A ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = sum_ x e. O ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) )
23	1	adantr	|- ( ( ph /\ x e. A ) -> O e. Fin )
24	2	adantr	|- ( ( ph /\ x e. A ) -> A C_ O )
25		simpr	|- ( ( ph /\ x e. A ) -> x e. A )
26		ind1	|- ( ( O e. Fin /\ A C_ O /\ x e. A ) -> ( ( ( _Ind ` O ) ` A ) ` x ) = 1 )
27	23 24 25 26	syl3anc	|- ( ( ph /\ x e. A ) -> ( ( ( _Ind ` O ) ` A ) ` x ) = 1 )
28	27	oveq1d	|- ( ( ph /\ x e. A ) -> ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = ( 1 x. B ) )
29	3	mullidd	|- ( ( ph /\ x e. O ) -> ( 1 x. B ) = B )
30	4 29	syldan	|- ( ( ph /\ x e. A ) -> ( 1 x. B ) = B )
31	28 30	eqtrd	|- ( ( ph /\ x e. A ) -> ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = B )
32	31	sumeq2dv	|- ( ph -> sum_ x e. A ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = sum_ x e. A B )
33	22 32	eqtr3d	|- ( ph -> sum_ x e. O ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = sum_ x e. A B )