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