Theorem offinsupp1

Description: Finite support for a function operation. (Contributed by Thierry Arnoux, 8-Jul-2023)

	Ref	Expression
Hypotheses	offinsupp1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	offinsupp1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
	offinsupp1.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
	offinsupp1.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
	offinsupp1.g	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑇 )
	offinsupp1.1	⊢ ( 𝜑 → 𝐹 finSupp 𝑌 )
	offinsupp1.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝑌 𝑅 𝑥 ) = 𝑍 )
Assertion	offinsupp1	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) finSupp 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		offinsupp1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		offinsupp1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
3		offinsupp1.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
4		offinsupp1.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
5		offinsupp1.g	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑇 )
6		offinsupp1.1	⊢ ( 𝜑 → 𝐹 finSupp 𝑌 )
7		offinsupp1.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝑌 𝑅 𝑥 ) = 𝑍 )
8	6	fsuppimpd	⊢ ( 𝜑 → ( 𝐹 supp 𝑌 ) ∈ Fin )
9		ssidd	⊢ ( 𝜑 → ( 𝐹 supp 𝑌 ) ⊆ ( 𝐹 supp 𝑌 ) )
10	9 7 4 5 1 2	suppssof1	⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) supp 𝑍 ) ⊆ ( 𝐹 supp 𝑌 ) )
11	8 10	ssfid	⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) supp 𝑍 ) ∈ Fin )
12		ovexd	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑆 ∧ 𝑗 ∈ 𝑇 ) ) → ( 𝑖 𝑅 𝑗 ) ∈ V )
13		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
14	12 4 5 1 1 13	off	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) : 𝐴 ⟶ V )
15	14	ffund	⊢ ( 𝜑 → Fun ( 𝐹 ∘f 𝑅 𝐺 ) )
16		ovexd	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) ∈ V )
17		funisfsupp	⊢ ( ( Fun ( 𝐹 ∘f 𝑅 𝐺 ) ∧ ( 𝐹 ∘f 𝑅 𝐺 ) ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝐹 ∘f 𝑅 𝐺 ) finSupp 𝑍 ↔ ( ( 𝐹 ∘f 𝑅 𝐺 ) supp 𝑍 ) ∈ Fin ) )
18	15 16 3 17	syl3anc	⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑅 𝐺 ) finSupp 𝑍 ↔ ( ( 𝐹 ∘f 𝑅 𝐺 ) supp 𝑍 ) ∈ Fin ) )
19	11 18	mpbird	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) finSupp 𝑍 )