# 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 ∈ W ∧ Z ∈ V → F supp Z = ∅ ↔ F = A × Z$

### Proof

Step Hyp Ref Expression
1 ss0b $⊢ F supp Z ⊆ ∅ ↔ F supp Z = ∅$
2 un0 $⊢ A ∪ ∅ = A$
3 uncom $⊢ A ∪ ∅ = ∅ ∪ A$
4 2 3 eqtr3i $⊢ A = ∅ ∪ A$
5 4 fneq2i $⊢ F Fn A ↔ F Fn ∅ ∪ A$
6 5 biimpi $⊢ F Fn A → F Fn ∅ ∪ A$
7 6 3ad2ant1 $⊢ F Fn A ∧ A ∈ W ∧ Z ∈ V → F Fn ∅ ∪ A$
8 fnex $⊢ F Fn A ∧ A ∈ W → F ∈ V$
9 8 3adant3 $⊢ F Fn A ∧ A ∈ W ∧ Z ∈ V → F ∈ V$
10 simp3 $⊢ F Fn A ∧ A ∈ W ∧ Z ∈ V → Z ∈ V$
11 0in $⊢ ∅ ∩ A = ∅$
12 11 a1i $⊢ F Fn A ∧ A ∈ W ∧ Z ∈ V → ∅ ∩ A = ∅$
13 fnsuppres $⊢ F Fn ∅ ∪ A ∧ F ∈ V ∧ Z ∈ V ∧ ∅ ∩ A = ∅ → F supp Z ⊆ ∅ ↔ F ↾ A = A × Z$
14 7 9 10 12 13 syl121anc $⊢ F Fn A ∧ A ∈ W ∧ Z ∈ V → F supp Z ⊆ ∅ ↔ F ↾ A = A × Z$
15 1 14 bitr3id $⊢ F Fn A ∧ A ∈ W ∧ Z ∈ V → F supp Z = ∅ ↔ F ↾ A = A × Z$
16 fnresdm $⊢ F Fn A → F ↾ A = F$
17 16 3ad2ant1 $⊢ F Fn A ∧ A ∈ W ∧ Z ∈ V → F ↾ A = F$
18 17 eqeq1d $⊢ F Fn A ∧ A ∈ W ∧ Z ∈ V → F ↾ A = A × Z ↔ F = A × Z$
19 15 18 bitrd $⊢ F Fn A ∧ A ∈ W ∧ Z ∈ V → F supp Z = ∅ ↔ F = A × Z$