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

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 
|- ( ph -> F finSupp Z )
fsuppco.g 
|- ( ph -> G : X -1-1-> Y )
fsuppco.z 
|- ( ph -> Z e. W )
fsuppco.v 
|- ( ph -> F e. V )
Assertion fsuppco 
|- ( ph -> ( F o. G ) finSupp Z )

Proof

Step Hyp Ref Expression
1 fsuppco.f 
 |-  ( ph -> F finSupp Z )
2 fsuppco.g 
 |-  ( ph -> G : X -1-1-> Y )
3 fsuppco.z 
 |-  ( ph -> Z e. W )
4 fsuppco.v 
 |-  ( ph -> F e. V )
5 df-f1 
 |-  ( G : X -1-1-> Y <-> ( G : X --> Y /\ Fun `' G ) )
6 5 simprbi 
 |-  ( G : X -1-1-> Y -> Fun `' G )
7 2 6 syl 
 |-  ( ph -> Fun `' G )
8 cofunex2g 
 |-  ( ( F e. V /\ Fun `' G ) -> ( F o. G ) e. _V )
9 4 7 8 syl2anc 
 |-  ( ph -> ( F o. G ) e. _V )
10 suppimacnv 
 |-  ( ( ( F o. G ) e. _V /\ Z e. W ) -> ( ( F o. G ) supp Z ) = ( `' ( F o. G ) " ( _V \ { Z } ) ) )
11 9 3 10 syl2anc 
 |-  ( ph -> ( ( F o. G ) supp Z ) = ( `' ( F o. G ) " ( _V \ { Z } ) ) )
12 suppimacnv 
 |-  ( ( F e. V /\ Z e. W ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
13 4 3 12 syl2anc 
 |-  ( ph -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
14 1 fsuppimpd 
 |-  ( ph -> ( F supp Z ) e. Fin )
15 13 14 eqeltrrd 
 |-  ( ph -> ( `' F " ( _V \ { Z } ) ) e. Fin )
16 15 2 fsuppcolem 
 |-  ( ph -> ( `' ( F o. G ) " ( _V \ { Z } ) ) e. Fin )
17 11 16 eqeltrd 
 |-  ( ph -> ( ( F o. G ) supp Z ) e. Fin )
18 fsuppimp 
 |-  ( F finSupp Z -> ( Fun F /\ ( F supp Z ) e. Fin ) )
19 18 simpld 
 |-  ( F finSupp Z -> Fun F )
20 1 19 syl 
 |-  ( ph -> Fun F )
21 f1fun 
 |-  ( G : X -1-1-> Y -> Fun G )
22 2 21 syl 
 |-  ( ph -> Fun G )
23 funco 
 |-  ( ( Fun F /\ Fun G ) -> Fun ( F o. G ) )
24 20 22 23 syl2anc 
 |-  ( ph -> Fun ( F o. G ) )
25 funisfsupp 
 |-  ( ( Fun ( F o. G ) /\ ( F o. G ) e. _V /\ Z e. W ) -> ( ( F o. G ) finSupp Z <-> ( ( F o. G ) supp Z ) e. Fin ) )
26 24 9 3 25 syl3anc 
 |-  ( ph -> ( ( F o. G ) finSupp Z <-> ( ( F o. G ) supp Z ) e. Fin ) )
27 17 26 mpbird 
 |-  ( ph -> ( F o. G ) finSupp Z )