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 
|- ( 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 )