Metamath Proof Explorer

Theorem fdifsupp

Description: Express the support of a function F outside of B in two different ways. (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses fdifsupp.1 
|- ( ph -> A e. V )
fdifsupp.2 
|- ( ph -> Z e. W )
fdifsupp.3 
|- ( ph -> F Fn A )
Assertion fdifsupp 
|- ( ph -> ( ( F |` ( A \ B ) ) supp Z ) = ( ( F supp Z ) \ B ) )

Proof

Step Hyp Ref Expression
1 fdifsupp.1 
 |-  ( ph -> A e. V )
2 fdifsupp.2 
 |-  ( ph -> Z e. W )
3 fdifsupp.3 
 |-  ( ph -> F Fn A )
4 difssd 
 |-  ( ph -> ( A \ B ) C_ A )
5 3 4 fnssresd 
 |-  ( ph -> ( F |` ( A \ B ) ) Fn ( A \ B ) )
6 1 difexd 
 |-  ( ph -> ( A \ B ) e. _V )
7 elsuppfn 
 |-  ( ( ( F |` ( A \ B ) ) Fn ( A \ B ) /\ ( A \ B ) e. _V /\ Z e. W ) -> ( x e. ( ( F |` ( A \ B ) ) supp Z ) <-> ( x e. ( A \ B ) /\ ( ( F |` ( A \ B ) ) ` x ) =/= Z ) ) )
8 5 6 2 7 syl3anc 
 |-  ( ph -> ( x e. ( ( F |` ( A \ B ) ) supp Z ) <-> ( x e. ( A \ B ) /\ ( ( F |` ( A \ B ) ) ` x ) =/= Z ) ) )
9 eldif 
 |-  ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
10 9 anbi1i 
 |-  ( ( x e. ( A \ B ) /\ ( F ` x ) =/= Z ) <-> ( ( x e. A /\ -. x e. B ) /\ ( F ` x ) =/= Z ) )
11 10 a1i 
 |-  ( ph -> ( ( x e. ( A \ B ) /\ ( F ` x ) =/= Z ) <-> ( ( x e. A /\ -. x e. B ) /\ ( F ` x ) =/= Z ) ) )
12 simpr 
 |-  ( ( ph /\ x e. ( A \ B ) ) -> x e. ( A \ B ) )
13 12 fvresd 
 |-  ( ( ph /\ x e. ( A \ B ) ) -> ( ( F |` ( A \ B ) ) ` x ) = ( F ` x ) )
14 13 neeq1d 
 |-  ( ( ph /\ x e. ( A \ B ) ) -> ( ( ( F |` ( A \ B ) ) ` x ) =/= Z <-> ( F ` x ) =/= Z ) )
15 14 pm5.32da 
 |-  ( ph -> ( ( x e. ( A \ B ) /\ ( ( F |` ( A \ B ) ) ` x ) =/= Z ) <-> ( x e. ( A \ B ) /\ ( F ` x ) =/= Z ) ) )
16 an32 
 |-  ( ( ( x e. A /\ ( F ` x ) =/= Z ) /\ -. x e. B ) <-> ( ( x e. A /\ -. x e. B ) /\ ( F ` x ) =/= Z ) )
17 16 a1i 
 |-  ( ph -> ( ( ( x e. A /\ ( F ` x ) =/= Z ) /\ -. x e. B ) <-> ( ( x e. A /\ -. x e. B ) /\ ( F ` x ) =/= Z ) ) )
18 11 15 17 3bitr4d 
 |-  ( ph -> ( ( x e. ( A \ B ) /\ ( ( F |` ( A \ B ) ) ` x ) =/= Z ) <-> ( ( x e. A /\ ( F ` x ) =/= Z ) /\ -. x e. B ) ) )
19 eldif 
 |-  ( x e. ( ( F supp Z ) \ B ) <-> ( x e. ( F supp Z ) /\ -. x e. B ) )
20 1 elexd 
 |-  ( ph -> A e. _V )
21 elsuppfn 
 |-  ( ( F Fn A /\ A e. _V /\ Z e. W ) -> ( x e. ( F supp Z ) <-> ( x e. A /\ ( F ` x ) =/= Z ) ) )
22 3 20 2 21 syl3anc 
 |-  ( ph -> ( x e. ( F supp Z ) <-> ( x e. A /\ ( F ` x ) =/= Z ) ) )
23 22 anbi1d 
 |-  ( ph -> ( ( x e. ( F supp Z ) /\ -. x e. B ) <-> ( ( x e. A /\ ( F ` x ) =/= Z ) /\ -. x e. B ) ) )
24 19 23 bitr2id 
 |-  ( ph -> ( ( ( x e. A /\ ( F ` x ) =/= Z ) /\ -. x e. B ) <-> x e. ( ( F supp Z ) \ B ) ) )
25 8 18 24 3bitrd 
 |-  ( ph -> ( x e. ( ( F |` ( A \ B ) ) supp Z ) <-> x e. ( ( F supp Z ) \ B ) ) )
26 25 eqrdv 
 |-  ( ph -> ( ( F |` ( A \ B ) ) supp Z ) = ( ( F supp Z ) \ B ) )