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