Metamath Proof Explorer

Theorem suppofss1d

Description: Condition for the support of a function operation to be a subset of the support of the left function term. (Contributed by Thierry Arnoux, 21-Jun-2019)

Ref Expression
Hypotheses suppofssd.1 
|- ( ph -> A e. V )
suppofssd.2 
|- ( ph -> Z e. B )
suppofssd.3 
|- ( ph -> F : A --> B )
suppofssd.4 
|- ( ph -> G : A --> B )
suppofss1d.5 
|- ( ( ph /\ x e. B ) -> ( Z X x ) = Z )
Assertion suppofss1d 
|- ( ph -> ( ( F oF X G ) supp Z ) C_ ( F supp Z ) )

Proof

Step Hyp Ref Expression
1 suppofssd.1 
 |-  ( ph -> A e. V )
2 suppofssd.2 
 |-  ( ph -> Z e. B )
3 suppofssd.3 
 |-  ( ph -> F : A --> B )
4 suppofssd.4 
 |-  ( ph -> G : A --> B )
5 suppofss1d.5 
 |-  ( ( ph /\ x e. B ) -> ( Z X x ) = Z )
6 3 ffnd 
 |-  ( ph -> F Fn A )
7 4 ffnd 
 |-  ( ph -> G Fn A )
8 inidm 
 |-  ( A i^i A ) = A
9 eqidd 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) = ( F ` y ) )
10 eqidd 
 |-  ( ( ph /\ y e. A ) -> ( G ` y ) = ( G ` y ) )
11 6 7 1 1 8 9 10 ofval 
 |-  ( ( ph /\ y e. A ) -> ( ( F oF X G ) ` y ) = ( ( F ` y ) X ( G ` y ) ) )
12 11 adantr 
 |-  ( ( ( ph /\ y e. A ) /\ ( F ` y ) = Z ) -> ( ( F oF X G ) ` y ) = ( ( F ` y ) X ( G ` y ) ) )
13 simpr 
 |-  ( ( ( ph /\ y e. A ) /\ ( F ` y ) = Z ) -> ( F ` y ) = Z )
14 13 oveq1d 
 |-  ( ( ( ph /\ y e. A ) /\ ( F ` y ) = Z ) -> ( ( F ` y ) X ( G ` y ) ) = ( Z X ( G ` y ) ) )
15 5 ralrimiva 
 |-  ( ph -> A. x e. B ( Z X x ) = Z )
16 15 adantr 
 |-  ( ( ph /\ y e. A ) -> A. x e. B ( Z X x ) = Z )
17 4 ffvelrnda 
 |-  ( ( ph /\ y e. A ) -> ( G ` y ) e. B )
18 simpr 
 |-  ( ( ( ph /\ y e. A ) /\ x = ( G ` y ) ) -> x = ( G ` y ) )
19 18 oveq2d 
 |-  ( ( ( ph /\ y e. A ) /\ x = ( G ` y ) ) -> ( Z X x ) = ( Z X ( G ` y ) ) )
20 19 eqeq1d 
 |-  ( ( ( ph /\ y e. A ) /\ x = ( G ` y ) ) -> ( ( Z X x ) = Z <-> ( Z X ( G ` y ) ) = Z ) )
21 17 20 rspcdv 
 |-  ( ( ph /\ y e. A ) -> ( A. x e. B ( Z X x ) = Z -> ( Z X ( G ` y ) ) = Z ) )
22 16 21 mpd 
 |-  ( ( ph /\ y e. A ) -> ( Z X ( G ` y ) ) = Z )
23 22 adantr 
 |-  ( ( ( ph /\ y e. A ) /\ ( F ` y ) = Z ) -> ( Z X ( G ` y ) ) = Z )
24 12 14 23 3eqtrd 
 |-  ( ( ( ph /\ y e. A ) /\ ( F ` y ) = Z ) -> ( ( F oF X G ) ` y ) = Z )
25 24 ex 
 |-  ( ( ph /\ y e. A ) -> ( ( F ` y ) = Z -> ( ( F oF X G ) ` y ) = Z ) )
26 25 ralrimiva 
 |-  ( ph -> A. y e. A ( ( F ` y ) = Z -> ( ( F oF X G ) ` y ) = Z ) )
27 6 7 1 1 8 offn 
 |-  ( ph -> ( F oF X G ) Fn A )
28 ssidd 
 |-  ( ph -> A C_ A )
29 suppfnss 
 |-  ( ( ( ( F oF X G ) Fn A /\ F Fn A ) /\ ( A C_ A /\ A e. V /\ Z e. B ) ) -> ( A. y e. A ( ( F ` y ) = Z -> ( ( F oF X G ) ` y ) = Z ) -> ( ( F oF X G ) supp Z ) C_ ( F supp Z ) ) )
30 27 6 28 1 2 29 syl23anc 
 |-  ( ph -> ( A. y e. A ( ( F ` y ) = Z -> ( ( F oF X G ) ` y ) = Z ) -> ( ( F oF X G ) supp Z ) C_ ( F supp Z ) ) )
31 26 30 mpd 
 |-  ( ph -> ( ( F oF X G ) supp Z ) C_ ( F supp Z ) )