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 } ) ) )