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 fex ⊢ ( ( 𝐺 : 𝐵 ⟶ 𝐷 ∧ 𝐵 ∈ 𝑉 ) → 𝐺 ∈ V )
29 4 7 28 syl2anc ⊢ ( 𝜑 → 𝐺 ∈ V )
30 fex ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐴 ∈ 𝑈 ) → 𝐹 ∈ V )
31 3 6 30 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ V )
32 coexg ⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ) → ( 𝐺 ∘ 𝐹 ) ∈ V )
33 29 31 32 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ∈ V )
34 isfsupp ⊢ ( ( ( 𝐺 ∘ 𝐹 ) ∈ V ∧ 0 ∈ 𝑊 ) → ( ( 𝐺 ∘ 𝐹 ) finSupp 0 ↔ ( Fun ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) supp 0 ) ∈ Fin ) ) )
35 33 1 34 syl2anc ⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) finSupp 0 ↔ ( Fun ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) supp 0 ) ∈ Fin ) ) )
36 13 27 35 mpbir2and ⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) finSupp 0 )