Metamath Proof Explorer

Theorem fsuppcor

Description: The composition of a function which maps the zero of the range of a finitely supported function to the zero of its range with this finitely supported function is finitely supported. (Contributed by AV, 6-Jun-2019)

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

Proof

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