Metamath Proof Explorer

Theorem suppco

Description: The support of the composition of two functions is the inverse image by the inner function of the support of the outer function. (Contributed by AV, 30-May-2019) Extract this statement from the proof of supp0cosupp0 . (Revised by SN, 15-Sep-2023)

Ref Expression
Assertion suppco ⊢ F ∈ V ∧ G ∈ W → F ∘ G supp Z = G -1 F supp Z

Proof

Step Hyp Ref Expression
1 coexg ⊢ F ∈ V ∧ G ∈ W → F ∘ G ∈ V
2 simpl ⊢ Z ∈ V ∧ F ∈ V ∧ G ∈ W → Z ∈ V
3 suppimacnv ⊢ F ∘ G ∈ V ∧ Z ∈ V → F ∘ G supp Z = F ∘ G -1 V ∖ Z
4 1 2 3 syl2an2 ⊢ Z ∈ V ∧ F ∈ V ∧ G ∈ W → F ∘ G supp Z = F ∘ G -1 V ∖ Z
5 cnvco ⊢ F ∘ G -1 = G -1 ∘ F -1
6 5 imaeq1i ⊢ F ∘ G -1 V ∖ Z = G -1 ∘ F -1 V ∖ Z
7 6 a1i ⊢ Z ∈ V ∧ F ∈ V ∧ G ∈ W → F ∘ G -1 V ∖ Z = G -1 ∘ F -1 V ∖ Z
8 imaco ⊢ G -1 ∘ F -1 V ∖ Z = G -1 F -1 V ∖ Z
9 simprl ⊢ Z ∈ V ∧ F ∈ V ∧ G ∈ W → F ∈ V
10 suppimacnv ⊢ F ∈ V ∧ Z ∈ V → F supp Z = F -1 V ∖ Z
11 9 2 10 syl2anc ⊢ Z ∈ V ∧ F ∈ V ∧ G ∈ W → F supp Z = F -1 V ∖ Z
12 11 imaeq2d ⊢ Z ∈ V ∧ F ∈ V ∧ G ∈ W → G -1 F supp Z = G -1 F -1 V ∖ Z
13 8 12 eqtr4id ⊢ Z ∈ V ∧ F ∈ V ∧ G ∈ W → G -1 ∘ F -1 V ∖ Z = G -1 F supp Z
14 4 7 13 3eqtrd ⊢ Z ∈ V ∧ F ∈ V ∧ G ∈ W → F ∘ G supp Z = G -1 F supp Z
15 14 ex ⊢ Z ∈ V → F ∈ V ∧ G ∈ W → F ∘ G supp Z = G -1 F supp Z
16 prcnel ⊢ ¬ Z ∈ V → ¬ Z ∈ V
17 16 intnand ⊢ ¬ Z ∈ V → ¬ F ∘ G ∈ V ∧ Z ∈ V
18 supp0prc ⊢ ¬ F ∘ G ∈ V ∧ Z ∈ V → F ∘ G supp Z = ∅
19 17 18 syl ⊢ ¬ Z ∈ V → F ∘ G supp Z = ∅
20 16 intnand ⊢ ¬ Z ∈ V → ¬ F ∈ V ∧ Z ∈ V
21 supp0prc ⊢ ¬ F ∈ V ∧ Z ∈ V → F supp Z = ∅
22 20 21 syl ⊢ ¬ Z ∈ V → F supp Z = ∅
23 22 imaeq2d ⊢ ¬ Z ∈ V → G -1 F supp Z = G -1 ∅
24 ima0 ⊢ G -1 ∅ = ∅
25 23 24 eqtrdi ⊢ ¬ Z ∈ V → G -1 F supp Z = ∅
26 19 25 eqtr4d ⊢ ¬ Z ∈ V → F ∘ G supp Z = G -1 F supp Z
27 26 a1d ⊢ ¬ Z ∈ V → F ∈ V ∧ G ∈ W → F ∘ G supp Z = G -1 F supp Z
28 15 27 pm2.61i ⊢ F ∈ V ∧ G ∈ W → F ∘ G supp Z = G -1 F supp Z