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 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
fsuppmptif.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
fsuppmptif.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
fsuppmptif.s ⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
Assertion fsuppmptif ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ) finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 fsuppmptif.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 fsuppmptif.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 fsuppmptif.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
4 fsuppmptif.s ⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
5 fvex ⊢ ( 𝐹 ‘ 𝑘 ) ∈ V
6 3 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑍 ∈ 𝑊 )
7 ifexg ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ V ∧ 𝑍 ∈ 𝑊 ) → if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ∈ V )
8 5 6 7 sylancr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ∈ V )
9 8 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ) : 𝐴 ⟶ V )
10 9 ffund ⊢ ( 𝜑 → Fun ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ) )
11 4 fsuppimpd ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
12 ssidd ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) )
13 1 12 2 3 suppssr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
14 13 ifeq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) = if ( 𝑘 ∈ 𝐷 , 𝑍 , 𝑍 ) )
15 ifid ⊢ if ( 𝑘 ∈ 𝐷 , 𝑍 , 𝑍 ) = 𝑍
16 14 15 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) = 𝑍 )
17 16 2 suppss2 ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ) supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) )
18 11 17 ssfid ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ) supp 𝑍 ) ∈ Fin )
19 2 mptexd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ) ∈ V )
20 isfsupp ⊢ ( ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ) ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ) finSupp 𝑍 ↔ ( Fun ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ) ∧ ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ) supp 𝑍 ) ∈ Fin ) ) )
21 19 3 20 syl2anc ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ) finSupp 𝑍 ↔ ( Fun ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ) ∧ ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ) supp 𝑍 ) ∈ Fin ) ) )
22 10 18 21 mpbir2and ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 ∈ 𝐷 , ( 𝐹 ‘ 𝑘 ) , 𝑍 ) ) finSupp 𝑍 )