Description: The support of the composition of two functions is empty if the support of the outer function is empty. (Contributed by AV, 30-May-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | supp0cosupp0 | ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( 𝐹 supp 𝑍 ) = ∅ → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) = ∅ ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | suppco | ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) = ( ◡ 𝐺 “ ( 𝐹 supp 𝑍 ) ) ) | |
2 | imaeq2 | ⊢ ( ( 𝐹 supp 𝑍 ) = ∅ → ( ◡ 𝐺 “ ( 𝐹 supp 𝑍 ) ) = ( ◡ 𝐺 “ ∅ ) ) | |
3 | ima0 | ⊢ ( ◡ 𝐺 “ ∅ ) = ∅ | |
4 | 2 3 | eqtrdi | ⊢ ( ( 𝐹 supp 𝑍 ) = ∅ → ( ◡ 𝐺 “ ( 𝐹 supp 𝑍 ) ) = ∅ ) |
5 | 1 4 | sylan9eq | ⊢ ( ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) ∧ ( 𝐹 supp 𝑍 ) = ∅ ) → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) = ∅ ) |
6 | 5 | ex | ⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( 𝐹 supp 𝑍 ) = ∅ → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) = ∅ ) ) |