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	4 7	fexd	\|- ( ph -> G e. _V )
29	3 6	fexd	\|- ( ph -> F e. _V )
30		coexg	\|- ( ( G e. _V /\ F e. _V ) -> ( G o. F ) e. _V )
31	28 29 30	syl2anc	\|- ( ph -> ( G o. F ) e. _V )
32		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 ) ) )
33	31 1 32	syl2anc	\|- ( ph -> ( ( G o. F ) finSupp .0. <-> ( Fun ( G o. F ) /\ ( ( G o. F ) supp .0. ) e. Fin ) ) )
34	13 27 33	mpbir2and	\|- ( ph -> ( G o. F ) finSupp .0. )

Metamath Proof Explorer

Theorem fsuppcor

Proof