Metamath Proof Explorer

Theorem suppcoss

Description: The support of the composition of two functions is a subset of the support of the inner function if the outer function preserves zero. Compare suppssfv , which has a sethood condition on A instead of B . (Contributed by SN, 25-May-2024)

Ref Expression
Hypotheses suppcoss.f ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
suppcoss.g ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
suppcoss.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
suppcoss.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
suppcoss.1 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) = 𝑍 )
Assertion suppcoss ( 𝜑 → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ⊆ ( 𝐺 supp 𝑌 ) )

Proof

Step Hyp Ref Expression
1 suppcoss.f ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2 suppcoss.g ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
3 suppcoss.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4 suppcoss.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
5 suppcoss.1 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) = 𝑍 )
6 dffn3 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 )
7 1 6 sylib ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ran 𝐹 )
8 7 2 fcod ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : 𝐵 ⟶ ran 𝐹 )
9 eldif ⊢ ( 𝑘 ∈ ( 𝐵 ∖ ( 𝐺 supp 𝑌 ) ) ↔ ( 𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ ( 𝐺 supp 𝑌 ) ) )
10 2 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
11 elsuppfn ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐵 ∈ 𝑊 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑘 ∈ ( 𝐺 supp 𝑌 ) ↔ ( 𝑘 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑌 ) ) )
12 10 3 4 11 syl3anc ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐺 supp 𝑌 ) ↔ ( 𝑘 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑌 ) ) )
13 12 notbid ⊢ ( 𝜑 → ( ¬ 𝑘 ∈ ( 𝐺 supp 𝑌 ) ↔ ¬ ( 𝑘 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑌 ) ) )
14 13 anbi2d ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ ( 𝐺 supp 𝑌 ) ) ↔ ( 𝑘 ∈ 𝐵 ∧ ¬ ( 𝑘 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑌 ) ) ) )
15 annotanannot ⊢ ( ( 𝑘 ∈ 𝐵 ∧ ¬ ( 𝑘 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑌 ) ) ↔ ( 𝑘 ∈ 𝐵 ∧ ¬ ( 𝐺 ‘ 𝑘 ) ≠ 𝑌 ) )
16 14 15 bitrdi ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ ( 𝐺 supp 𝑌 ) ) ↔ ( 𝑘 ∈ 𝐵 ∧ ¬ ( 𝐺 ‘ 𝑘 ) ≠ 𝑌 ) ) )
17 9 16 bitrid ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐵 ∖ ( 𝐺 supp 𝑌 ) ) ↔ ( 𝑘 ∈ 𝐵 ∧ ¬ ( 𝐺 ‘ 𝑘 ) ≠ 𝑌 ) ) )
18 nne ⊢ ( ¬ ( 𝐺 ‘ 𝑘 ) ≠ 𝑌 ↔ ( 𝐺 ‘ 𝑘 ) = 𝑌 )
19 18 anbi2i ⊢ ( ( 𝑘 ∈ 𝐵 ∧ ¬ ( 𝐺 ‘ 𝑘 ) ≠ 𝑌 ) ↔ ( 𝑘 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑌 ) )
20 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑌 ) ) → 𝐺 : 𝐵 ⟶ 𝐴 )
21 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑌 ) ) → 𝑘 ∈ 𝐵 )
22 20 21 fvco3d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑌 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
23 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑌 ) ) → ( 𝐺 ‘ 𝑘 ) = 𝑌 )
24 23 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑌 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝑌 ) )
25 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑌 ) ) → ( 𝐹 ‘ 𝑌 ) = 𝑍 )
26 22 24 25 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑌 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑘 ) = 𝑍 )
27 26 ex ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑌 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑘 ) = 𝑍 ) )
28 19 27 biimtrid ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐵 ∧ ¬ ( 𝐺 ‘ 𝑘 ) ≠ 𝑌 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑘 ) = 𝑍 ) )
29 17 28 sylbid ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐵 ∖ ( 𝐺 supp 𝑌 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑘 ) = 𝑍 ) )
30 29 imp ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( 𝐺 supp 𝑌 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑘 ) = 𝑍 )
31 8 30 suppss ⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) ⊆ ( 𝐺 supp 𝑌 ) )