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 𝑍 ) = ∅ ↔ 𝐹 = ( 𝐴 × { 𝑍 } ) ) )