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𝑊 )
fsuppcor.z ( 𝜑𝑍𝐵 )
fsuppcor.f ( 𝜑𝐹 : 𝐴𝐶 )
fsuppcor.g ( 𝜑𝐺 : 𝐵𝐷 )
fsuppcor.s ( 𝜑𝐶𝐵 )
fsuppcor.a ( 𝜑𝐴𝑈 )
fsuppcor.b ( 𝜑𝐵𝑉 )
fsuppcor.n ( 𝜑𝐹 finSupp 𝑍 )
fsuppcor.i ( 𝜑 → ( 𝐺𝑍 ) = 0 )
Assertion fsuppcor ( 𝜑 → ( 𝐺𝐹 ) finSupp 0 )

Proof

Step Hyp Ref Expression
1 fsuppcor.0 ( 𝜑0𝑊 )
2 fsuppcor.z ( 𝜑𝑍𝐵 )
3 fsuppcor.f ( 𝜑𝐹 : 𝐴𝐶 )
4 fsuppcor.g ( 𝜑𝐺 : 𝐵𝐷 )
5 fsuppcor.s ( 𝜑𝐶𝐵 )
6 fsuppcor.a ( 𝜑𝐴𝑈 )
7 fsuppcor.b ( 𝜑𝐵𝑉 )
8 fsuppcor.n ( 𝜑𝐹 finSupp 𝑍 )
9 fsuppcor.i ( 𝜑 → ( 𝐺𝑍 ) = 0 )
10 4 ffund ( 𝜑 → Fun 𝐺 )
11 3 ffund ( 𝜑 → Fun 𝐹 )
12 funco ( ( Fun 𝐺 ∧ Fun 𝐹 ) → Fun ( 𝐺𝐹 ) )
13 10 11 12 syl2anc ( 𝜑 → Fun ( 𝐺𝐹 ) )
14 8 fsuppimpd ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
15 4 5 fssresd ( 𝜑 → ( 𝐺𝐶 ) : 𝐶𝐷 )
16 fco2 ( ( ( 𝐺𝐶 ) : 𝐶𝐷𝐹 : 𝐴𝐶 ) → ( 𝐺𝐹 ) : 𝐴𝐷 )
17 15 3 16 syl2anc ( 𝜑 → ( 𝐺𝐹 ) : 𝐴𝐷 )
18 eldifi ( 𝑥 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) → 𝑥𝐴 )
19 fvco3 ( ( 𝐹 : 𝐴𝐶𝑥𝐴 ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹𝑥 ) ) )
20 3 18 19 syl2an ( ( 𝜑𝑥 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐹𝑥 ) ) )
21 ssidd ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐹 supp 𝑍 ) )
22 3 21 6 2 suppssr ( ( 𝜑𝑥 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → ( 𝐹𝑥 ) = 𝑍 )
23 22 fveq2d ( ( 𝜑𝑥 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → ( 𝐺 ‘ ( 𝐹𝑥 ) ) = ( 𝐺𝑍 ) )
24 9 adantr ( ( 𝜑𝑥 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → ( 𝐺𝑍 ) = 0 )
25 20 23 24 3eqtrd ( ( 𝜑𝑥 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) ) → ( ( 𝐺𝐹 ) ‘ 𝑥 ) = 0 )
26 17 25 suppss ( 𝜑 → ( ( 𝐺𝐹 ) supp 0 ) ⊆ ( 𝐹 supp 𝑍 ) )
27 14 26 ssfid ( 𝜑 → ( ( 𝐺𝐹 ) supp 0 ) ∈ Fin )
28 4 7 fexd ( 𝜑𝐺 ∈ V )
29 3 6 fexd ( 𝜑𝐹 ∈ V )
30 coexg ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ) → ( 𝐺𝐹 ) ∈ V )
31 28 29 30 syl2anc ( 𝜑 → ( 𝐺𝐹 ) ∈ V )
32 isfsupp ( ( ( 𝐺𝐹 ) ∈ V ∧ 0𝑊 ) → ( ( 𝐺𝐹 ) finSupp 0 ↔ ( Fun ( 𝐺𝐹 ) ∧ ( ( 𝐺𝐹 ) supp 0 ) ∈ Fin ) ) )
33 31 1 32 syl2anc ( 𝜑 → ( ( 𝐺𝐹 ) finSupp 0 ↔ ( Fun ( 𝐺𝐹 ) ∧ ( ( 𝐺𝐹 ) supp 0 ) ∈ Fin ) ) )
34 13 27 33 mpbir2and ( 𝜑 → ( 𝐺𝐹 ) finSupp 0 )