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 bitrid 
 |-  ( 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 biimtrid 
 |-  ( 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 ) )