Metamath Proof Explorer

Theorem mptnn0fsupp

Description: A mapping from the nonnegative integers is finitely supported under certain conditions. (Contributed by AV, 5-Oct-2019) (Revised by AV, 23-Dec-2019)

Ref Expression
Hypotheses mptnn0fsupp.0 
|- ( ph -> .0. e. V )
mptnn0fsupp.c 
|- ( ( ph /\ k e. NN0 ) -> C e. B )
mptnn0fsupp.s 
|- ( ph -> E. s e. NN0 A. x e. NN0 ( s < x -> [_ x / k ]_ C = .0. ) )
Assertion mptnn0fsupp 
|- ( ph -> ( k e. NN0 |-> C ) finSupp .0. )

Proof

Step Hyp Ref Expression
1 mptnn0fsupp.0 
 |-  ( ph -> .0. e. V )
2 mptnn0fsupp.c 
 |-  ( ( ph /\ k e. NN0 ) -> C e. B )
3 mptnn0fsupp.s 
 |-  ( ph -> E. s e. NN0 A. x e. NN0 ( s < x -> [_ x / k ]_ C = .0. ) )
4 2 ralrimiva 
 |-  ( ph -> A. k e. NN0 C e. B )
5 eqid 
 |-  ( k e. NN0 |-> C ) = ( k e. NN0 |-> C )
6 5 fnmpt 
 |-  ( A. k e. NN0 C e. B -> ( k e. NN0 |-> C ) Fn NN0 )
7 4 6 syl 
 |-  ( ph -> ( k e. NN0 |-> C ) Fn NN0 )
8 nn0ex 
 |-  NN0 e. _V
9 8 a1i 
 |-  ( ph -> NN0 e. _V )
10 1 elexd 
 |-  ( ph -> .0. e. _V )
11 suppvalfn 
 |-  ( ( ( k e. NN0 |-> C ) Fn NN0 /\ NN0 e. _V /\ .0. e. _V ) -> ( ( k e. NN0 |-> C ) supp .0. ) = { x e. NN0 | ( ( k e. NN0 |-> C ) ` x ) =/= .0. } )
12 7 9 10 11 syl3anc 
 |-  ( ph -> ( ( k e. NN0 |-> C ) supp .0. ) = { x e. NN0 | ( ( k e. NN0 |-> C ) ` x ) =/= .0. } )
13 nne 
 |-  ( -. ( ( k e. NN0 |-> C ) ` x ) =/= .0. <-> ( ( k e. NN0 |-> C ) ` x ) = .0. )
14 simpr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ x e. NN0 ) -> x e. NN0 )
15 4 ad2antrr 
 |-  ( ( ( ph /\ s e. NN0 ) /\ x e. NN0 ) -> A. k e. NN0 C e. B )
16 rspcsbela 
 |-  ( ( x e. NN0 /\ A. k e. NN0 C e. B ) -> [_ x / k ]_ C e. B )
17 14 15 16 syl2anc 
 |-  ( ( ( ph /\ s e. NN0 ) /\ x e. NN0 ) -> [_ x / k ]_ C e. B )
18 5 fvmpts 
 |-  ( ( x e. NN0 /\ [_ x / k ]_ C e. B ) -> ( ( k e. NN0 |-> C ) ` x ) = [_ x / k ]_ C )
19 14 17 18 syl2anc 
 |-  ( ( ( ph /\ s e. NN0 ) /\ x e. NN0 ) -> ( ( k e. NN0 |-> C ) ` x ) = [_ x / k ]_ C )
20 19 eqeq1d 
 |-  ( ( ( ph /\ s e. NN0 ) /\ x e. NN0 ) -> ( ( ( k e. NN0 |-> C ) ` x ) = .0. <-> [_ x / k ]_ C = .0. ) )
21 13 20 bitrid 
 |-  ( ( ( ph /\ s e. NN0 ) /\ x e. NN0 ) -> ( -. ( ( k e. NN0 |-> C ) ` x ) =/= .0. <-> [_ x / k ]_ C = .0. ) )
22 21 imbi2d 
 |-  ( ( ( ph /\ s e. NN0 ) /\ x e. NN0 ) -> ( ( s < x -> -. ( ( k e. NN0 |-> C ) ` x ) =/= .0. ) <-> ( s < x -> [_ x / k ]_ C = .0. ) ) )
23 22 ralbidva 
 |-  ( ( ph /\ s e. NN0 ) -> ( A. x e. NN0 ( s < x -> -. ( ( k e. NN0 |-> C ) ` x ) =/= .0. ) <-> A. x e. NN0 ( s < x -> [_ x / k ]_ C = .0. ) ) )
24 23 rexbidva 
 |-  ( ph -> ( E. s e. NN0 A. x e. NN0 ( s < x -> -. ( ( k e. NN0 |-> C ) ` x ) =/= .0. ) <-> E. s e. NN0 A. x e. NN0 ( s < x -> [_ x / k ]_ C = .0. ) ) )
25 3 24 mpbird 
 |-  ( ph -> E. s e. NN0 A. x e. NN0 ( s < x -> -. ( ( k e. NN0 |-> C ) ` x ) =/= .0. ) )
26 rabssnn0fi 
 |-  ( { x e. NN0 | ( ( k e. NN0 |-> C ) ` x ) =/= .0. } e. Fin <-> E. s e. NN0 A. x e. NN0 ( s < x -> -. ( ( k e. NN0 |-> C ) ` x ) =/= .0. ) )
27 25 26 sylibr 
 |-  ( ph -> { x e. NN0 | ( ( k e. NN0 |-> C ) ` x ) =/= .0. } e. Fin )
28 12 27 eqeltrd 
 |-  ( ph -> ( ( k e. NN0 |-> C ) supp .0. ) e. Fin )
29 funmpt 
 |-  Fun ( k e. NN0 |-> C )
30 8 mptex 
 |-  ( k e. NN0 |-> C ) e. _V
31 funisfsupp 
 |-  ( ( Fun ( k e. NN0 |-> C ) /\ ( k e. NN0 |-> C ) e. _V /\ .0. e. _V ) -> ( ( k e. NN0 |-> C ) finSupp .0. <-> ( ( k e. NN0 |-> C ) supp .0. ) e. Fin ) )
32 29 30 10 31 mp3an12i 
 |-  ( ph -> ( ( k e. NN0 |-> C ) finSupp .0. <-> ( ( k e. NN0 |-> C ) supp .0. ) e. Fin ) )
33 28 32 mpbird 
 |-  ( ph -> ( k e. NN0 |-> C ) finSupp .0. )