Metamath Proof Explorer

Theorem fdifsuppconst

Description: A function is a zero constant outside of its support. (Contributed by Thierry Arnoux, 22-Jun-2024)

Ref Expression
Hypothesis fdifsuppconst.1 
|- A = ( dom F \ ( F supp Z ) )
Assertion fdifsuppconst 
|- ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F |` A ) = ( A X. { Z } ) )

Proof

Step Hyp Ref Expression
1 fdifsuppconst.1 
 |-  A = ( dom F \ ( F supp Z ) )
2 funfn 
 |-  ( Fun F <-> F Fn dom F )
3 2 biimpi 
 |-  ( Fun F -> F Fn dom F )
4 3 ad2antrr 
 |-  ( ( ( Fun F /\ F e. V ) /\ Z e. W ) -> F Fn dom F )
5 difssd 
 |-  ( ( ( Fun F /\ F e. V ) /\ Z e. W ) -> ( dom F \ ( F supp Z ) ) C_ dom F )
6 1 5 eqsstrid 
 |-  ( ( ( Fun F /\ F e. V ) /\ Z e. W ) -> A C_ dom F )
7 4 6 fnssresd 
 |-  ( ( ( Fun F /\ F e. V ) /\ Z e. W ) -> ( F |` A ) Fn A )
8 fnconstg 
 |-  ( Z e. W -> ( A X. { Z } ) Fn A )
9 8 adantl 
 |-  ( ( ( Fun F /\ F e. V ) /\ Z e. W ) -> ( A X. { Z } ) Fn A )
10 4 adantr 
 |-  ( ( ( ( Fun F /\ F e. V ) /\ Z e. W ) /\ x e. A ) -> F Fn dom F )
11 dmexg 
 |-  ( F e. V -> dom F e. _V )
12 11 ad3antlr 
 |-  ( ( ( ( Fun F /\ F e. V ) /\ Z e. W ) /\ x e. A ) -> dom F e. _V )
13 simplr 
 |-  ( ( ( ( Fun F /\ F e. V ) /\ Z e. W ) /\ x e. A ) -> Z e. W )
14 1 eleq2i 
 |-  ( x e. A <-> x e. ( dom F \ ( F supp Z ) ) )
15 14 biimpi 
 |-  ( x e. A -> x e. ( dom F \ ( F supp Z ) ) )
16 15 adantl 
 |-  ( ( ( ( Fun F /\ F e. V ) /\ Z e. W ) /\ x e. A ) -> x e. ( dom F \ ( F supp Z ) ) )
17 10 12 13 16 fvdifsupp 
 |-  ( ( ( ( Fun F /\ F e. V ) /\ Z e. W ) /\ x e. A ) -> ( F ` x ) = Z )
18 simpr 
 |-  ( ( ( ( Fun F /\ F e. V ) /\ Z e. W ) /\ x e. A ) -> x e. A )
19 18 fvresd 
 |-  ( ( ( ( Fun F /\ F e. V ) /\ Z e. W ) /\ x e. A ) -> ( ( F |` A ) ` x ) = ( F ` x ) )
20 fvconst2g 
 |-  ( ( Z e. W /\ x e. A ) -> ( ( A X. { Z } ) ` x ) = Z )
21 20 adantll 
 |-  ( ( ( ( Fun F /\ F e. V ) /\ Z e. W ) /\ x e. A ) -> ( ( A X. { Z } ) ` x ) = Z )
22 17 19 21 3eqtr4d 
 |-  ( ( ( ( Fun F /\ F e. V ) /\ Z e. W ) /\ x e. A ) -> ( ( F |` A ) ` x ) = ( ( A X. { Z } ) ` x ) )
23 7 9 22 eqfnfvd 
 |-  ( ( ( Fun F /\ F e. V ) /\ Z e. W ) -> ( F |` A ) = ( A X. { Z } ) )
24 23 3impa 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F |` A ) = ( A X. { Z } ) )