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 ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉 ) → ( ( 𝐹 supp 𝑍 ) = ∅ ↔ 𝐹 = ( 𝐴 × { 𝑍 } ) ) )

Proof

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