This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnsuppeq0

Description: The support of a function is empty iff it is identically zero. (Contributed by Stefan O'Rear, 22-Mar-2015) (Revised by AV, 28-May-2019)

Ref Expression
Assertion fnsuppeq0 
|- ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( ( F supp Z ) = (/) <-> F = ( A X. { Z } ) ) )

Proof

Step Hyp Ref Expression
1 ss0b 
 |-  ( ( F supp Z ) C_ (/) <-> ( F supp Z ) = (/) )
2 un0 
 |-  ( A u. (/) ) = A
3 uncom 
 |-  ( A u. (/) ) = ( (/) u. A )
4 2 3 eqtr3i 
 |-  A = ( (/) u. A )
5 4 fneq2i 
 |-  ( F Fn A <-> F Fn ( (/) u. A ) )
6 5 biimpi 
 |-  ( F Fn A -> F Fn ( (/) u. A ) )
7 6 3ad2ant1 
 |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> F Fn ( (/) u. A ) )
8 fnex 
 |-  ( ( F Fn A /\ A e. W ) -> F e. _V )
9 8 3adant3 
 |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> F e. _V )
10 simp3 
 |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> Z e. V )
11 0in 
 |-  ( (/) i^i A ) = (/)
12 11 a1i 
 |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( (/) i^i A ) = (/) )
13 fnsuppres 
 |-  ( ( F Fn ( (/) u. A ) /\ ( F e. _V /\ Z e. V ) /\ ( (/) i^i A ) = (/) ) -> ( ( F supp Z ) C_ (/) <-> ( F |` A ) = ( A X. { Z } ) ) )
14 7 9 10 12 13 syl121anc 
 |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( ( F supp Z ) C_ (/) <-> ( F |` A ) = ( A X. { Z } ) ) )
15 1 14 bitr3id 
 |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( ( F supp Z ) = (/) <-> ( F |` A ) = ( A X. { Z } ) ) )
16 fnresdm 
 |-  ( F Fn A -> ( F |` A ) = F )
17 16 3ad2ant1 
 |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( F |` A ) = F )
18 17 eqeq1d 
 |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( ( F |` A ) = ( A X. { Z } ) <-> F = ( A X. { Z } ) ) )
19 15 18 bitrd 
 |-  ( ( F Fn A /\ A e. W /\ Z e. V ) -> ( ( F supp Z ) = (/) <-> F = ( A X. { Z } ) ) )