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 ( ( 𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊 ) → ( ( 𝐹 ∘ 𝐺 ) supp 𝑍 ) = ( ◡ 𝐺 “ ( 𝐹 supp 𝑍 ) ) )

Proof

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