Metamath Proof Explorer

Theorem fsuppmptif

Description: A function mapping an argument to either a value of a finitely supported function or zero is finitely supported. (Contributed by AV, 6-Jun-2019)

Ref Expression
Hypotheses fsuppmptif.f 
|- ( ph -> F : A --> B )
fsuppmptif.a 
|- ( ph -> A e. V )
fsuppmptif.z 
|- ( ph -> Z e. W )
fsuppmptif.s 
|- ( ph -> F finSupp Z )
Assertion fsuppmptif 
|- ( ph -> ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) finSupp Z )

Proof

Step Hyp Ref Expression
1 fsuppmptif.f 
 |-  ( ph -> F : A --> B )
2 fsuppmptif.a 
 |-  ( ph -> A e. V )
3 fsuppmptif.z 
 |-  ( ph -> Z e. W )
4 fsuppmptif.s 
 |-  ( ph -> F finSupp Z )
5 fvex 
 |-  ( F ` k ) e. _V
6 3 adantr 
 |-  ( ( ph /\ k e. A ) -> Z e. W )
7 ifexg 
 |-  ( ( ( F ` k ) e. _V /\ Z e. W ) -> if ( k e. D , ( F ` k ) , Z ) e. _V )
8 5 6 7 sylancr 
 |-  ( ( ph /\ k e. A ) -> if ( k e. D , ( F ` k ) , Z ) e. _V )
9 8 fmpttd 
 |-  ( ph -> ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) : A --> _V )
10 9 ffund 
 |-  ( ph -> Fun ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) )
11 4 fsuppimpd 
 |-  ( ph -> ( F supp Z ) e. Fin )
12 ssidd 
 |-  ( ph -> ( F supp Z ) C_ ( F supp Z ) )
13 1 12 2 3 suppssr 
 |-  ( ( ph /\ k e. ( A \ ( F supp Z ) ) ) -> ( F ` k ) = Z )
14 13 ifeq1d 
 |-  ( ( ph /\ k e. ( A \ ( F supp Z ) ) ) -> if ( k e. D , ( F ` k ) , Z ) = if ( k e. D , Z , Z ) )
15 ifid 
 |-  if ( k e. D , Z , Z ) = Z
16 14 15 eqtrdi 
 |-  ( ( ph /\ k e. ( A \ ( F supp Z ) ) ) -> if ( k e. D , ( F ` k ) , Z ) = Z )
17 16 2 suppss2 
 |-  ( ph -> ( ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) supp Z ) C_ ( F supp Z ) )
18 11 17 ssfid 
 |-  ( ph -> ( ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) supp Z ) e. Fin )
19 2 mptexd 
 |-  ( ph -> ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) e. _V )
20 isfsupp 
 |-  ( ( ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) e. _V /\ Z e. W ) -> ( ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) finSupp Z <-> ( Fun ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) /\ ( ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) supp Z ) e. Fin ) ) )
21 19 3 20 syl2anc 
 |-  ( ph -> ( ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) finSupp Z <-> ( Fun ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) /\ ( ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) supp Z ) e. Fin ) ) )
22 10 18 21 mpbir2and 
 |-  ( ph -> ( k e. A |-> if ( k e. D , ( F ` k ) , Z ) ) finSupp Z )