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 𝑍 )