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 3 5 fexd
 |-  ( ph -> G e. _V )
26 2 4 fexd
 |-  ( ph -> F e. _V )
27 coexg
 |-  ( ( G e. _V /\ F e. _V ) -> ( G o. F ) e. _V )
28 25 26 27 syl2anc
 |-  ( ph -> ( G o. F ) e. _V )
29 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 ) ) )
30 28 1 29 syl2anc
 |-  ( ph -> ( ( G o. F ) finSupp Z <-> ( Fun ( G o. F ) /\ ( ( G o. F ) supp Z ) e. Fin ) ) )
31 11 24 30 mpbir2and
 |-  ( ph -> ( G o. F ) finSupp Z )