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