Metamath Proof Explorer


Theorem fsuppmapnn0fiub0

Description: If all functions of a finite set of functions over the nonnegative integers are finitely supported, then all these functions are zero for all integers greater than a fixed integer. (Contributed by AV, 3-Oct-2019)

Ref Expression
Assertion fsuppmapnn0fiub0 M R 0 M Fin Z V f M finSupp Z f m 0 f M x 0 m < x f x = Z

Proof

Step Hyp Ref Expression
1 fsuppmapnn0fiubex M R 0 M Fin Z V f M finSupp Z f m 0 f M f supp Z 0 m
2 ssel2 M R 0 f M f R 0
3 2 ancoms f M M R 0 f R 0
4 elmapfn f R 0 f Fn 0
5 3 4 syl f M M R 0 f Fn 0
6 5 expcom M R 0 f M f Fn 0
7 6 3ad2ant1 M R 0 M Fin Z V f M f Fn 0
8 7 adantr M R 0 M Fin Z V m 0 f M f Fn 0
9 8 imp M R 0 M Fin Z V m 0 f M f Fn 0
10 nn0ex 0 V
11 10 a1i M R 0 M Fin Z V m 0 f M 0 V
12 simpll3 M R 0 M Fin Z V m 0 f M Z V
13 suppvalfn f Fn 0 0 V Z V f supp Z = x 0 | f x Z
14 9 11 12 13 syl3anc M R 0 M Fin Z V m 0 f M f supp Z = x 0 | f x Z
15 14 sseq1d M R 0 M Fin Z V m 0 f M f supp Z 0 m x 0 | f x Z 0 m
16 rabss x 0 | f x Z 0 m x 0 f x Z x 0 m
17 15 16 bitrdi M R 0 M Fin Z V m 0 f M f supp Z 0 m x 0 f x Z x 0 m
18 nne ¬ f x Z f x = Z
19 18 biimpi ¬ f x Z f x = Z
20 19 2a1d ¬ f x Z M R 0 M Fin Z V m 0 f M x 0 m < x f x = Z
21 elfz2nn0 x 0 m x 0 m 0 x m
22 nn0re x 0 x
23 nn0re m 0 m
24 lenlt x m x m ¬ m < x
25 22 23 24 syl2an x 0 m 0 x m ¬ m < x
26 pm2.21 ¬ m < x m < x f x = Z
27 25 26 syl6bi x 0 m 0 x m m < x f x = Z
28 27 3impia x 0 m 0 x m m < x f x = Z
29 28 a1d x 0 m 0 x m M R 0 M Fin Z V m 0 f M x 0 m < x f x = Z
30 21 29 sylbi x 0 m M R 0 M Fin Z V m 0 f M x 0 m < x f x = Z
31 20 30 ja f x Z x 0 m M R 0 M Fin Z V m 0 f M x 0 m < x f x = Z
32 31 com12 M R 0 M Fin Z V m 0 f M x 0 f x Z x 0 m m < x f x = Z
33 32 ralimdva M R 0 M Fin Z V m 0 f M x 0 f x Z x 0 m x 0 m < x f x = Z
34 17 33 sylbid M R 0 M Fin Z V m 0 f M f supp Z 0 m x 0 m < x f x = Z
35 34 ralimdva M R 0 M Fin Z V m 0 f M f supp Z 0 m f M x 0 m < x f x = Z
36 35 reximdva M R 0 M Fin Z V m 0 f M f supp Z 0 m m 0 f M x 0 m < x f x = Z
37 1 36 syld M R 0 M Fin Z V f M finSupp Z f m 0 f M x 0 m < x f x = Z