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 syl5bb ( 𝜑 → ( 𝑘 ∈ ( 𝐵 ∖ ( 𝐺 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 syl5bi ( 𝜑 → ( ( 𝑘𝐵 ∧ ¬ ( 𝐺𝑘 ) ≠ 𝑌 ) → ( ( 𝐹𝐺 ) ‘ 𝑘 ) = 𝑍 ) )
29 17 28 sylbid ( 𝜑 → ( 𝑘 ∈ ( 𝐵 ∖ ( 𝐺 supp 𝑌 ) ) → ( ( 𝐹𝐺 ) ‘ 𝑘 ) = 𝑍 ) )
30 29 imp ( ( 𝜑𝑘 ∈ ( 𝐵 ∖ ( 𝐺 supp 𝑌 ) ) ) → ( ( 𝐹𝐺 ) ‘ 𝑘 ) = 𝑍 )
31 8 30 suppss ( 𝜑 → ( ( 𝐹𝐺 ) supp 𝑍 ) ⊆ ( 𝐺 supp 𝑌 ) )