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 φ 0 ˙ W
fsuppcor.z φ Z B
fsuppcor.f φ F : A C
fsuppcor.g φ G : B D
fsuppcor.s φ C B
fsuppcor.a φ A U
fsuppcor.b φ B V
fsuppcor.n φ finSupp Z F
fsuppcor.i φ G Z = 0 ˙
Assertion fsuppcor φ finSupp 0 ˙ G F

Proof

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