Metamath Proof Explorer

Theorem fsumsupp0

Description: Finite sum of function values, for a function of finite support. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses fsumsupp0.a 
|- ( ph -> A e. Fin )
fsumsupp0.f 
|- ( ph -> F : A --> CC )
Assertion fsumsupp0 
|- ( ph -> sum_ k e. ( F supp 0 ) ( F ` k ) = sum_ k e. A ( F ` k ) )

Proof

Step Hyp Ref Expression
1 fsumsupp0.a 
 |-  ( ph -> A e. Fin )
2 fsumsupp0.f 
 |-  ( ph -> F : A --> CC )
3 2 ffnd 
 |-  ( ph -> F Fn A )
4 0red 
 |-  ( ph -> 0 e. RR )
5 suppvalfn 
 |-  ( ( F Fn A /\ A e. Fin /\ 0 e. RR ) -> ( F supp 0 ) = { k e. A | ( F ` k ) =/= 0 } )
6 3 1 4 5 syl3anc 
 |-  ( ph -> ( F supp 0 ) = { k e. A | ( F ` k ) =/= 0 } )
7 ssrab2 
 |-  { k e. A | ( F ` k ) =/= 0 } C_ A
8 6 7 eqsstrdi 
 |-  ( ph -> ( F supp 0 ) C_ A )
9 2 adantr 
 |-  ( ( ph /\ k e. ( F supp 0 ) ) -> F : A --> CC )
10 8 sselda 
 |-  ( ( ph /\ k e. ( F supp 0 ) ) -> k e. A )
11 9 10 ffvelrnd 
 |-  ( ( ph /\ k e. ( F supp 0 ) ) -> ( F ` k ) e. CC )
12 eldifi 
 |-  ( k e. ( A \ ( F supp 0 ) ) -> k e. A )
13 12 adantr 
 |-  ( ( k e. ( A \ ( F supp 0 ) ) /\ -. ( F ` k ) = 0 ) -> k e. A )
14 neqne 
 |-  ( -. ( F ` k ) = 0 -> ( F ` k ) =/= 0 )
15 14 adantl 
 |-  ( ( k e. ( A \ ( F supp 0 ) ) /\ -. ( F ` k ) = 0 ) -> ( F ` k ) =/= 0 )
16 13 15 jca 
 |-  ( ( k e. ( A \ ( F supp 0 ) ) /\ -. ( F ` k ) = 0 ) -> ( k e. A /\ ( F ` k ) =/= 0 ) )
17 rabid 
 |-  ( k e. { k e. A | ( F ` k ) =/= 0 } <-> ( k e. A /\ ( F ` k ) =/= 0 ) )
18 16 17 sylibr 
 |-  ( ( k e. ( A \ ( F supp 0 ) ) /\ -. ( F ` k ) = 0 ) -> k e. { k e. A | ( F ` k ) =/= 0 } )
19 18 adantll 
 |-  ( ( ( ph /\ k e. ( A \ ( F supp 0 ) ) ) /\ -. ( F ` k ) = 0 ) -> k e. { k e. A | ( F ` k ) =/= 0 } )
20 6 eleq2d 
 |-  ( ph -> ( k e. ( F supp 0 ) <-> k e. { k e. A | ( F ` k ) =/= 0 } ) )
21 20 ad2antrr 
 |-  ( ( ( ph /\ k e. ( A \ ( F supp 0 ) ) ) /\ -. ( F ` k ) = 0 ) -> ( k e. ( F supp 0 ) <-> k e. { k e. A | ( F ` k ) =/= 0 } ) )
22 19 21 mpbird 
 |-  ( ( ( ph /\ k e. ( A \ ( F supp 0 ) ) ) /\ -. ( F ` k ) = 0 ) -> k e. ( F supp 0 ) )
23 eldifn 
 |-  ( k e. ( A \ ( F supp 0 ) ) -> -. k e. ( F supp 0 ) )
24 23 ad2antlr 
 |-  ( ( ( ph /\ k e. ( A \ ( F supp 0 ) ) ) /\ -. ( F ` k ) = 0 ) -> -. k e. ( F supp 0 ) )
25 22 24 condan 
 |-  ( ( ph /\ k e. ( A \ ( F supp 0 ) ) ) -> ( F ` k ) = 0 )
26 8 11 25 1 fsumss 
 |-  ( ph -> sum_ k e. ( F supp 0 ) ( F ` k ) = sum_ k e. A ( F ` k ) )