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		fex	⊢ ( ( 𝐺 : 𝐵 ⟶ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐺 ∈ V )
26	3 5 25	syl2anc	⊢ ( 𝜑 → 𝐺 ∈ V )
27		fex	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑈 ) → 𝐹 ∈ V )
28	2 4 27	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ V )
29		coexg	⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ) → ( 𝐺 ∘ 𝐹 ) ∈ V )
30	26 28 29	syl2anc	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) ∈ V )
31		isfsupp	⊢ ( ( ( 𝐺 ∘ 𝐹 ) ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐺 ∘ 𝐹 ) finSupp 𝑍 ↔ ( Fun ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) supp 𝑍 ) ∈ Fin ) ) )
32	30 1 31	syl2anc	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) finSupp 𝑍 ↔ ( Fun ( 𝐺 ∘ 𝐹 ) ∧ ( ( 𝐺 ∘ 𝐹 ) supp 𝑍 ) ∈ Fin ) ) )
33	11 24 32	mpbir2and	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) finSupp 𝑍 )