This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resfsupp

Description: If the restriction of a function by a set which, subtracted from the domain of the function so that its difference is finitely supported, the function itself is finitely supported. (Contributed by AV, 27-May-2019)

Ref Expression
Hypotheses resfsupp.b ⊢ φ → dom ⁡ F ∖ B ∈ Fin
resfsupp.e ⊢ φ → F ∈ W
resfsupp.f ⊢ φ → Fun ⁡ F
resfsupp.g ⊢ φ → G = F ↾ B
resfsupp.s ⊢ φ → finSupp Z⁡ G
resfsupp.z ⊢ φ → Z ∈ V
Assertion resfsupp ⊢ φ → finSupp Z⁡ F

Proof

Step Hyp Ref Expression
1 resfsupp.b ⊢ φ → dom ⁡ F ∖ B ∈ Fin
2 resfsupp.e ⊢ φ → F ∈ W
3 resfsupp.f ⊢ φ → Fun ⁡ F
4 resfsupp.g ⊢ φ → G = F ↾ B
5 resfsupp.s ⊢ φ → finSupp Z⁡ G
6 resfsupp.z ⊢ φ → Z ∈ V
7 5 fsuppimpd ⊢ φ → G supp Z ∈ Fin
8 1 2 4 7 6 ressuppfi ⊢ φ → F supp Z ∈ Fin
9 funisfsupp ⊢ Fun ⁡ F ∧ F ∈ W ∧ Z ∈ V → finSupp Z⁡ F ↔ F supp Z ∈ Fin
10 3 2 6 9 syl3anc ⊢ φ → finSupp Z⁡ F ↔ F supp Z ∈ Fin
11 8 10 mpbird ⊢ φ → finSupp Z⁡ F