Metamath Proof Explorer

Theorem fsuppco

Description: The composition of a 1-1 function with a finitely supported function is finitely supported. (Contributed by AV, 28-May-2019)

Ref Expression
Hypotheses fsuppco.f ⊢ φ → finSupp Z⁡ F
fsuppco.g ⊢ φ → G : X ⟶ 1-1 Y
fsuppco.z ⊢ φ → Z ∈ W
fsuppco.v ⊢ φ → F ∈ V
Assertion fsuppco ⊢ φ → finSupp Z⁡ F ∘ G

Proof

Step Hyp Ref Expression
1 fsuppco.f ⊢ φ → finSupp Z⁡ F
2 fsuppco.g ⊢ φ → G : X ⟶ 1-1 Y
3 fsuppco.z ⊢ φ → Z ∈ W
4 fsuppco.v ⊢ φ → F ∈ V
5 df-f1 ⊢ G : X ⟶ 1-1 Y ↔ G : X ⟶ Y ∧ Fun ⁡ G -1
6 5 simprbi ⊢ G : X ⟶ 1-1 Y → Fun ⁡ G -1
7 2 6 syl ⊢ φ → Fun ⁡ G -1
8 cofunex2g ⊢ F ∈ V ∧ Fun ⁡ G -1 → F ∘ G ∈ V
9 4 7 8 syl2anc ⊢ φ → F ∘ G ∈ V
10 suppimacnv ⊢ F ∘ G ∈ V ∧ Z ∈ W → F ∘ G supp Z = F ∘ G -1 V ∖ Z
11 9 3 10 syl2anc ⊢ φ → F ∘ G supp Z = F ∘ G -1 V ∖ Z
12 suppimacnv ⊢ F ∈ V ∧ Z ∈ W → F supp Z = F -1 V ∖ Z
13 4 3 12 syl2anc ⊢ φ → F supp Z = F -1 V ∖ Z
14 1 fsuppimpd ⊢ φ → F supp Z ∈ Fin
15 13 14 eqeltrrd ⊢ φ → F -1 V ∖ Z ∈ Fin
16 15 2 fsuppcolem ⊢ φ → F ∘ G -1 V ∖ Z ∈ Fin
17 11 16 eqeltrd ⊢ φ → F ∘ G supp Z ∈ Fin
18 fsuppimp ⊢ finSupp Z⁡ F → Fun ⁡ F ∧ F supp Z ∈ Fin
19 18 simpld ⊢ finSupp Z⁡ F → Fun ⁡ F
20 1 19 syl ⊢ φ → Fun ⁡ F
21 f1fun ⊢ G : X ⟶ 1-1 Y → Fun ⁡ G
22 2 21 syl ⊢ φ → Fun ⁡ G
23 funco ⊢ Fun ⁡ F ∧ Fun ⁡ G → Fun ⁡ F ∘ G
24 20 22 23 syl2anc ⊢ φ → Fun ⁡ F ∘ G
25 funisfsupp ⊢ Fun ⁡ F ∘ G ∧ F ∘ G ∈ V ∧ Z ∈ W → finSupp Z⁡ F ∘ G ↔ F ∘ G supp Z ∈ Fin
26 24 9 3 25 syl3anc ⊢ φ → finSupp Z⁡ F ∘ G ↔ F ∘ G supp Z ∈ Fin
27 17 26 mpbird ⊢ φ → finSupp Z⁡ F ∘ G