Metamath Proof Explorer

Theorem indsum

Description: Finite sum of a product with the indicator function / Cartesian product with the indicator function. (Contributed by Thierry Arnoux, 14-Aug-2017)

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 pr01ssre 
 |-  { 0 , 1 } C_ RR
6 indf 
 |-  ( ( O e. Fin /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) : O --> { 0 , 1 } )
7 1 2 6 syl2anc 
 |-  ( ph -> ( ( _Ind ` O ) ` A ) : O --> { 0 , 1 } )
8 7 ffvelrnda 
 |-  ( ( ph /\ x e. O ) -> ( ( ( _Ind ` O ) ` A ) ` x ) e. { 0 , 1 } )
9 5 8 sselid 
 |-  ( ( ph /\ x e. O ) -> ( ( ( _Ind ` O ) ` A ) ` x ) e. RR )
10 9 recnd 
 |-  ( ( ph /\ x e. O ) -> ( ( ( _Ind ` O ) ` A ) ` x ) e. CC )
11 10 3 mulcld 
 |-  ( ( ph /\ x e. O ) -> ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) e. CC )
12 4 11 syldan 
 |-  ( ( ph /\ x e. A ) -> ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) e. CC )
13 1 adantr 
 |-  ( ( ph /\ x e. ( O \ A ) ) -> O e. Fin )
14 2 adantr 
 |-  ( ( ph /\ x e. ( O \ A ) ) -> A C_ O )
15 simpr 
 |-  ( ( ph /\ x e. ( O \ A ) ) -> x e. ( O \ A ) )
16 ind0 
 |-  ( ( O e. Fin /\ A C_ O /\ x e. ( O \ A ) ) -> ( ( ( _Ind ` O ) ` A ) ` x ) = 0 )
17 13 14 15 16 syl3anc 
 |-  ( ( ph /\ x e. ( O \ A ) ) -> ( ( ( _Ind ` O ) ` A ) ` x ) = 0 )
18 17 oveq1d 
 |-  ( ( ph /\ x e. ( O \ A ) ) -> ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = ( 0 x. B ) )
19 difssd 
 |-  ( ph -> ( O \ A ) C_ O )
20 19 sselda 
 |-  ( ( ph /\ x e. ( O \ A ) ) -> x e. O )
21 3 mul02d 
 |-  ( ( ph /\ x e. O ) -> ( 0 x. B ) = 0 )
22 20 21 syldan 
 |-  ( ( ph /\ x e. ( O \ A ) ) -> ( 0 x. B ) = 0 )
23 18 22 eqtrd 
 |-  ( ( ph /\ x e. ( O \ A ) ) -> ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = 0 )
24 2 12 23 1 fsumss 
 |-  ( ph -> sum_ x e. A ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = sum_ x e. O ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) )
25 1 adantr 
 |-  ( ( ph /\ x e. A ) -> O e. Fin )
26 2 adantr 
 |-  ( ( ph /\ x e. A ) -> A C_ O )
27 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
28 ind1 
 |-  ( ( O e. Fin /\ A C_ O /\ x e. A ) -> ( ( ( _Ind ` O ) ` A ) ` x ) = 1 )
29 25 26 27 28 syl3anc 
 |-  ( ( ph /\ x e. A ) -> ( ( ( _Ind ` O ) ` A ) ` x ) = 1 )
30 29 oveq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = ( 1 x. B ) )
31 3 mulid2d 
 |-  ( ( ph /\ x e. O ) -> ( 1 x. B ) = B )
32 4 31 syldan 
 |-  ( ( ph /\ x e. A ) -> ( 1 x. B ) = B )
33 30 32 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = B )
34 33 sumeq2dv 
 |-  ( ph -> sum_ x e. A ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = sum_ x e. A B )
35 24 34 eqtr3d 
 |-  ( ph -> sum_ x e. O ( ( ( ( _Ind ` O ) ` A ) ` x ) x. B ) = sum_ x e. A B )