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

Proof

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