Metamath Proof Explorer

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 
|- ( ph -> O e. V )
indsumin.2 
|- ( ph -> A e. Fin )
indsumin.3 
|- ( ph -> A C_ O )
indsumin.4 
|- ( ph -> B C_ O )
indsumin.5 
|- ( ( ph /\ k e. A ) -> C e. CC )
Assertion indsumin 
|- ( ph -> sum_ k e. A ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) = sum_ k e. ( A i^i B ) C )

Proof

Step Hyp Ref Expression
1 indsumin.1 
 |-  ( ph -> O e. V )
2 indsumin.2 
 |-  ( ph -> A e. Fin )
3 indsumin.3 
 |-  ( ph -> A C_ O )
4 indsumin.4 
 |-  ( ph -> B C_ O )
5 indsumin.5 
 |-  ( ( ph /\ k e. A ) -> C e. CC )
6 inindif 
 |-  ( ( A i^i B ) i^i ( A \ B ) ) = (/)
7 6 a1i 
 |-  ( ph -> ( ( A i^i B ) i^i ( A \ B ) ) = (/) )
8 inundif 
 |-  ( ( A i^i B ) u. ( A \ B ) ) = A
9 8 eqcomi 
 |-  A = ( ( A i^i B ) u. ( A \ B ) )
10 9 a1i 
 |-  ( ph -> A = ( ( A i^i B ) u. ( A \ B ) ) )
11 pr01ssre 
 |-  { 0 , 1 } C_ RR
12 ax-resscn 
 |-  RR C_ CC
13 11 12 sstri 
 |-  { 0 , 1 } C_ CC
14 indf 
 |-  ( ( O e. V /\ B C_ O ) -> ( ( _Ind ` O ) ` B ) : O --> { 0 , 1 } )
15 1 4 14 syl2anc 
 |-  ( ph -> ( ( _Ind ` O ) ` B ) : O --> { 0 , 1 } )
16 15 adantr 
 |-  ( ( ph /\ k e. A ) -> ( ( _Ind ` O ) ` B ) : O --> { 0 , 1 } )
17 3 sselda 
 |-  ( ( ph /\ k e. A ) -> k e. O )
18 16 17 ffvelrnd 
 |-  ( ( ph /\ k e. A ) -> ( ( ( _Ind ` O ) ` B ) ` k ) e. { 0 , 1 } )
19 13 18 sseldi 
 |-  ( ( ph /\ k e. A ) -> ( ( ( _Ind ` O ) ` B ) ` k ) e. CC )
20 19 5 mulcld 
 |-  ( ( ph /\ k e. A ) -> ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) e. CC )
21 7 10 2 20 fsumsplit 
 |-  ( ph -> sum_ k e. A ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) = ( sum_ k e. ( A i^i B ) ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) + sum_ k e. ( A \ B ) ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) ) )
22 1 adantr 
 |-  ( ( ph /\ k e. ( A i^i B ) ) -> O e. V )
23 4 adantr 
 |-  ( ( ph /\ k e. ( A i^i B ) ) -> B C_ O )
24 inss2 
 |-  ( A i^i B ) C_ B
25 24 a1i 
 |-  ( ph -> ( A i^i B ) C_ B )
26 25 sselda 
 |-  ( ( ph /\ k e. ( A i^i B ) ) -> k e. B )
27 ind1 
 |-  ( ( O e. V /\ B C_ O /\ k e. B ) -> ( ( ( _Ind ` O ) ` B ) ` k ) = 1 )
28 22 23 26 27 syl3anc 
 |-  ( ( ph /\ k e. ( A i^i B ) ) -> ( ( ( _Ind ` O ) ` B ) ` k ) = 1 )
29 28 oveq1d 
 |-  ( ( ph /\ k e. ( A i^i B ) ) -> ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) = ( 1 x. C ) )
30 inss1 
 |-  ( A i^i B ) C_ A
31 30 a1i 
 |-  ( ph -> ( A i^i B ) C_ A )
32 31 sselda 
 |-  ( ( ph /\ k e. ( A i^i B ) ) -> k e. A )
33 32 5 syldan 
 |-  ( ( ph /\ k e. ( A i^i B ) ) -> C e. CC )
34 33 mulid2d 
 |-  ( ( ph /\ k e. ( A i^i B ) ) -> ( 1 x. C ) = C )
35 29 34 eqtrd 
 |-  ( ( ph /\ k e. ( A i^i B ) ) -> ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) = C )
36 35 sumeq2dv 
 |-  ( ph -> sum_ k e. ( A i^i B ) ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) = sum_ k e. ( A i^i B ) C )
37 1 adantr 
 |-  ( ( ph /\ k e. ( A \ B ) ) -> O e. V )
38 4 adantr 
 |-  ( ( ph /\ k e. ( A \ B ) ) -> B C_ O )
39 3 ssdifd 
 |-  ( ph -> ( A \ B ) C_ ( O \ B ) )
40 39 sselda 
 |-  ( ( ph /\ k e. ( A \ B ) ) -> k e. ( O \ B ) )
41 ind0 
 |-  ( ( O e. V /\ B C_ O /\ k e. ( O \ B ) ) -> ( ( ( _Ind ` O ) ` B ) ` k ) = 0 )
42 37 38 40 41 syl3anc 
 |-  ( ( ph /\ k e. ( A \ B ) ) -> ( ( ( _Ind ` O ) ` B ) ` k ) = 0 )
43 42 oveq1d 
 |-  ( ( ph /\ k e. ( A \ B ) ) -> ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) = ( 0 x. C ) )
44 difssd 
 |-  ( ph -> ( A \ B ) C_ A )
45 44 sselda 
 |-  ( ( ph /\ k e. ( A \ B ) ) -> k e. A )
46 45 5 syldan 
 |-  ( ( ph /\ k e. ( A \ B ) ) -> C e. CC )
47 46 mul02d 
 |-  ( ( ph /\ k e. ( A \ B ) ) -> ( 0 x. C ) = 0 )
48 43 47 eqtrd 
 |-  ( ( ph /\ k e. ( A \ B ) ) -> ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) = 0 )
49 48 sumeq2dv 
 |-  ( ph -> sum_ k e. ( A \ B ) ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) = sum_ k e. ( A \ B ) 0 )
50 diffi 
 |-  ( A e. Fin -> ( A \ B ) e. Fin )
51 2 50 syl 
 |-  ( ph -> ( A \ B ) e. Fin )
52 sumz 
 |-  ( ( ( A \ B ) C_ ( ZZ>= ` 0 ) \/ ( A \ B ) e. Fin ) -> sum_ k e. ( A \ B ) 0 = 0 )
53 52 olcs 
 |-  ( ( A \ B ) e. Fin -> sum_ k e. ( A \ B ) 0 = 0 )
54 51 53 syl 
 |-  ( ph -> sum_ k e. ( A \ B ) 0 = 0 )
55 49 54 eqtrd 
 |-  ( ph -> sum_ k e. ( A \ B ) ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) = 0 )
56 36 55 oveq12d 
 |-  ( ph -> ( sum_ k e. ( A i^i B ) ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) + sum_ k e. ( A \ B ) ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) ) = ( sum_ k e. ( A i^i B ) C + 0 ) )
57 infi 
 |-  ( A e. Fin -> ( A i^i B ) e. Fin )
58 2 57 syl 
 |-  ( ph -> ( A i^i B ) e. Fin )
59 58 33 fsumcl 
 |-  ( ph -> sum_ k e. ( A i^i B ) C e. CC )
60 59 addid1d 
 |-  ( ph -> ( sum_ k e. ( A i^i B ) C + 0 ) = sum_ k e. ( A i^i B ) C )
61 21 56 60 3eqtrd 
 |-  ( ph -> sum_ k e. A ( ( ( ( _Ind ` O ) ` B ) ` k ) x. C ) = sum_ k e. ( A i^i B ) C )