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 e. V /\ G e. W ) -> ( ( F o. G ) supp Z ) = ( `' G " ( F supp Z ) ) )

Proof

Step Hyp Ref Expression
1 coexg 
 |-  ( ( F e. V /\ G e. W ) -> ( F o. G ) e. _V )
2 simpl 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> Z e. _V )
3 suppimacnv 
 |-  ( ( ( F o. G ) e. _V /\ Z e. _V ) -> ( ( F o. G ) supp Z ) = ( `' ( F o. G ) " ( _V \ { Z } ) ) )
4 1 2 3 syl2an2 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( ( F o. G ) supp Z ) = ( `' ( F o. G ) " ( _V \ { Z } ) ) )
5 cnvco 
 |-  `' ( F o. G ) = ( `' G o. `' F )
6 5 imaeq1i 
 |-  ( `' ( F o. G ) " ( _V \ { Z } ) ) = ( ( `' G o. `' F ) " ( _V \ { Z } ) )
7 6 a1i 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( `' ( F o. G ) " ( _V \ { Z } ) ) = ( ( `' G o. `' F ) " ( _V \ { Z } ) ) )
8 imaco 
 |-  ( ( `' G o. `' F ) " ( _V \ { Z } ) ) = ( `' G " ( `' F " ( _V \ { Z } ) ) )
9 simprl 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> F e. V )
10 suppimacnv 
 |-  ( ( F e. V /\ Z e. _V ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
11 9 2 10 syl2anc 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
12 11 imaeq2d 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( `' G " ( F supp Z ) ) = ( `' G " ( `' F " ( _V \ { Z } ) ) ) )
13 8 12 eqtr4id 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( ( `' G o. `' F ) " ( _V \ { Z } ) ) = ( `' G " ( F supp Z ) ) )
14 4 7 13 3eqtrd 
 |-  ( ( Z e. _V /\ ( F e. V /\ G e. W ) ) -> ( ( F o. G ) supp Z ) = ( `' G " ( F supp Z ) ) )
15 14 ex 
 |-  ( Z e. _V -> ( ( F e. V /\ G e. W ) -> ( ( F o. G ) supp Z ) = ( `' G " ( F supp Z ) ) ) )
16 prcnel 
 |-  ( -. Z e. _V -> -. Z e. _V )
17 16 intnand 
 |-  ( -. Z e. _V -> -. ( ( F o. G ) e. _V /\ Z e. _V ) )
18 supp0prc 
 |-  ( -. ( ( F o. G ) e. _V /\ Z e. _V ) -> ( ( F o. G ) supp Z ) = (/) )
19 17 18 syl 
 |-  ( -. Z e. _V -> ( ( F o. G ) supp Z ) = (/) )
20 16 intnand 
 |-  ( -. Z e. _V -> -. ( F e. _V /\ Z e. _V ) )
21 supp0prc 
 |-  ( -. ( F e. _V /\ Z e. _V ) -> ( F supp Z ) = (/) )
22 20 21 syl 
 |-  ( -. Z e. _V -> ( F supp Z ) = (/) )
23 22 imaeq2d 
 |-  ( -. Z e. _V -> ( `' G " ( F supp Z ) ) = ( `' G " (/) ) )
24 ima0 
 |-  ( `' G " (/) ) = (/)
25 23 24 eqtrdi 
 |-  ( -. Z e. _V -> ( `' G " ( F supp Z ) ) = (/) )
26 19 25 eqtr4d 
 |-  ( -. Z e. _V -> ( ( F o. G ) supp Z ) = ( `' G " ( F supp Z ) ) )
27 26 a1d 
 |-  ( -. Z e. _V -> ( ( F e. V /\ G e. W ) -> ( ( F o. G ) supp Z ) = ( `' G " ( F supp Z ) ) ) )
28 15 27 pm2.61i 
 |-  ( ( F e. V /\ G e. W ) -> ( ( F o. G ) supp Z ) = ( `' G " ( F supp Z ) ) )