This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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