Metamath Proof Explorer

Theorem fsuppco2

Description: The composition of a function which maps the zero to zero with a finitely supported function is finitely supported. This is not only a special case of fsuppcor because it does not require that the "zero" is an element of the range of the finitely supported function. (Contributed by AV, 6-Jun-2019)

Ref Expression
Hypotheses fsuppco2.z 
|- ( ph -> Z e. W )
fsuppco2.f 
|- ( ph -> F : A --> B )
fsuppco2.g 
|- ( ph -> G : B --> B )
fsuppco2.a 
|- ( ph -> A e. U )
fsuppco2.b 
|- ( ph -> B e. V )
fsuppco2.n 
|- ( ph -> F finSupp Z )
fsuppco2.i 
|- ( ph -> ( G ` Z ) = Z )
Assertion fsuppco2 
|- ( ph -> ( G o. F ) finSupp Z )

Proof

Step Hyp Ref Expression
1 fsuppco2.z 
 |-  ( ph -> Z e. W )
2 fsuppco2.f 
 |-  ( ph -> F : A --> B )
3 fsuppco2.g 
 |-  ( ph -> G : B --> B )
4 fsuppco2.a 
 |-  ( ph -> A e. U )
5 fsuppco2.b 
 |-  ( ph -> B e. V )
6 fsuppco2.n 
 |-  ( ph -> F finSupp Z )
7 fsuppco2.i 
 |-  ( ph -> ( G ` Z ) = Z )
8 3 ffund 
 |-  ( ph -> Fun G )
9 2 ffund 
 |-  ( ph -> Fun F )
10 funco 
 |-  ( ( Fun G /\ Fun F ) -> Fun ( G o. F ) )
11 8 9 10 syl2anc 
 |-  ( ph -> Fun ( G o. F ) )
12 6 fsuppimpd 
 |-  ( ph -> ( F supp Z ) e. Fin )
13 fco 
 |-  ( ( G : B --> B /\ F : A --> B ) -> ( G o. F ) : A --> B )
14 3 2 13 syl2anc 
 |-  ( ph -> ( G o. F ) : A --> B )
15 eldifi 
 |-  ( x e. ( A \ ( F supp Z ) ) -> x e. A )
16 fvco3 
 |-  ( ( F : A --> B /\ x e. A ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
17 2 15 16 syl2an 
 |-  ( ( ph /\ x e. ( A \ ( F supp Z ) ) ) -> ( ( G o. F ) ` x ) = ( G ` ( F ` x ) ) )
18 ssidd 
 |-  ( ph -> ( F supp Z ) C_ ( F supp Z ) )
19 2 18 4 1 suppssr 
 |-  ( ( ph /\ x e. ( A \ ( F supp Z ) ) ) -> ( F ` x ) = Z )
20 19 fveq2d 
 |-  ( ( ph /\ x e. ( A \ ( F supp Z ) ) ) -> ( G ` ( F ` x ) ) = ( G ` Z ) )
21 7 adantr 
 |-  ( ( ph /\ x e. ( A \ ( F supp Z ) ) ) -> ( G ` Z ) = Z )
22 17 20 21 3eqtrd 
 |-  ( ( ph /\ x e. ( A \ ( F supp Z ) ) ) -> ( ( G o. F ) ` x ) = Z )
23 14 22 suppss 
 |-  ( ph -> ( ( G o. F ) supp Z ) C_ ( F supp Z ) )
24 12 23 ssfid 
 |-  ( ph -> ( ( G o. F ) supp Z ) e. Fin )
25 fex 
 |-  ( ( G : B --> B /\ B e. V ) -> G e. _V )
26 3 5 25 syl2anc 
 |-  ( ph -> G e. _V )
27 fex 
 |-  ( ( F : A --> B /\ A e. U ) -> F e. _V )
28 2 4 27 syl2anc 
 |-  ( ph -> F e. _V )
29 coexg 
 |-  ( ( G e. _V /\ F e. _V ) -> ( G o. F ) e. _V )
30 26 28 29 syl2anc 
 |-  ( ph -> ( G o. F ) e. _V )
31 isfsupp 
 |-  ( ( ( G o. F ) e. _V /\ Z e. W ) -> ( ( G o. F ) finSupp Z <-> ( Fun ( G o. F ) /\ ( ( G o. F ) supp Z ) e. Fin ) ) )
32 30 1 31 syl2anc 
 |-  ( ph -> ( ( G o. F ) finSupp Z <-> ( Fun ( G o. F ) /\ ( ( G o. F ) supp Z ) e. Fin ) ) )
33 11 24 32 mpbir2and 
 |-  ( ph -> ( G o. F ) finSupp Z )