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
|- ( ph -> F Fn A )
suppcoss.g
|- ( ph -> G : B --> A )
suppcoss.b
|- ( ph -> B e. W )
suppcoss.y
|- ( ph -> Y e. V )
suppcoss.1
|- ( ph -> ( F ` Y ) = Z )
Assertion suppcoss
|- ( ph -> ( ( F o. G ) supp Z ) C_ ( G supp Y ) )

Proof

Step Hyp Ref Expression
1 suppcoss.f
 |-  ( ph -> F Fn A )
2 suppcoss.g
 |-  ( ph -> G : B --> A )
3 suppcoss.b
 |-  ( ph -> B e. W )
4 suppcoss.y
 |-  ( ph -> Y e. V )
5 suppcoss.1
 |-  ( ph -> ( F ` Y ) = Z )
6 dffn3
 |-  ( F Fn A <-> F : A --> ran F )
7 1 6 sylib
 |-  ( ph -> F : A --> ran F )
8 7 2 fcod
 |-  ( ph -> ( F o. G ) : B --> ran F )
9 eldif
 |-  ( k e. ( B \ ( G supp Y ) ) <-> ( k e. B /\ -. k e. ( G supp Y ) ) )
10 2 ffnd
 |-  ( ph -> G Fn B )
11 elsuppfn
 |-  ( ( G Fn B /\ B e. W /\ Y e. V ) -> ( k e. ( G supp Y ) <-> ( k e. B /\ ( G ` k ) =/= Y ) ) )
12 10 3 4 11 syl3anc
 |-  ( ph -> ( k e. ( G supp Y ) <-> ( k e. B /\ ( G ` k ) =/= Y ) ) )
13 12 notbid
 |-  ( ph -> ( -. k e. ( G supp Y ) <-> -. ( k e. B /\ ( G ` k ) =/= Y ) ) )
14 13 anbi2d
 |-  ( ph -> ( ( k e. B /\ -. k e. ( G supp Y ) ) <-> ( k e. B /\ -. ( k e. B /\ ( G ` k ) =/= Y ) ) ) )
15 annotanannot
 |-  ( ( k e. B /\ -. ( k e. B /\ ( G ` k ) =/= Y ) ) <-> ( k e. B /\ -. ( G ` k ) =/= Y ) )
16 14 15 bitrdi
 |-  ( ph -> ( ( k e. B /\ -. k e. ( G supp Y ) ) <-> ( k e. B /\ -. ( G ` k ) =/= Y ) ) )
17 9 16 syl5bb
 |-  ( ph -> ( k e. ( B \ ( G supp Y ) ) <-> ( k e. B /\ -. ( G ` k ) =/= Y ) ) )
18 nne
 |-  ( -. ( G ` k ) =/= Y <-> ( G ` k ) = Y )
19 18 anbi2i
 |-  ( ( k e. B /\ -. ( G ` k ) =/= Y ) <-> ( k e. B /\ ( G ` k ) = Y ) )
20 2 adantr
 |-  ( ( ph /\ ( k e. B /\ ( G ` k ) = Y ) ) -> G : B --> A )
21 simprl
 |-  ( ( ph /\ ( k e. B /\ ( G ` k ) = Y ) ) -> k e. B )
22 20 21 fvco3d
 |-  ( ( ph /\ ( k e. B /\ ( G ` k ) = Y ) ) -> ( ( F o. G ) ` k ) = ( F ` ( G ` k ) ) )
23 simprr
 |-  ( ( ph /\ ( k e. B /\ ( G ` k ) = Y ) ) -> ( G ` k ) = Y )
24 23 fveq2d
 |-  ( ( ph /\ ( k e. B /\ ( G ` k ) = Y ) ) -> ( F ` ( G ` k ) ) = ( F ` Y ) )
25 5 adantr
 |-  ( ( ph /\ ( k e. B /\ ( G ` k ) = Y ) ) -> ( F ` Y ) = Z )
26 22 24 25 3eqtrd
 |-  ( ( ph /\ ( k e. B /\ ( G ` k ) = Y ) ) -> ( ( F o. G ) ` k ) = Z )
27 26 ex
 |-  ( ph -> ( ( k e. B /\ ( G ` k ) = Y ) -> ( ( F o. G ) ` k ) = Z ) )
28 19 27 syl5bi
 |-  ( ph -> ( ( k e. B /\ -. ( G ` k ) =/= Y ) -> ( ( F o. G ) ` k ) = Z ) )
29 17 28 sylbid
 |-  ( ph -> ( k e. ( B \ ( G supp Y ) ) -> ( ( F o. G ) ` k ) = Z ) )
30 29 imp
 |-  ( ( ph /\ k e. ( B \ ( G supp Y ) ) ) -> ( ( F o. G ) ` k ) = Z )
31 8 30 suppss
 |-  ( ph -> ( ( F o. G ) supp Z ) C_ ( G supp Y ) )