Description: The support of the composition of two functions is empty if the support of the outer function is empty. (Contributed by AV, 30-May-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | supp0cosupp0 | |- ( ( F e. V /\ G e. W ) -> ( ( F supp Z ) = (/) -> ( ( F o. G ) supp Z ) = (/) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | suppco | |- ( ( F e. V /\ G e. W ) -> ( ( F o. G ) supp Z ) = ( `' G " ( F supp Z ) ) ) |
|
2 | imaeq2 | |- ( ( F supp Z ) = (/) -> ( `' G " ( F supp Z ) ) = ( `' G " (/) ) ) |
|
3 | ima0 | |- ( `' G " (/) ) = (/) |
|
4 | 2 3 | eqtrdi | |- ( ( F supp Z ) = (/) -> ( `' G " ( F supp Z ) ) = (/) ) |
5 | 1 4 | sylan9eq | |- ( ( ( F e. V /\ G e. W ) /\ ( F supp Z ) = (/) ) -> ( ( F o. G ) supp Z ) = (/) ) |
6 | 5 | ex | |- ( ( F e. V /\ G e. W ) -> ( ( F supp Z ) = (/) -> ( ( F o. G ) supp Z ) = (/) ) ) |