This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvdifsupp

Description: Function value is zero outside of its support. (Contributed by Thierry Arnoux, 21-Jan-2024)

Ref Expression
Hypotheses fvdifsupp.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
fvdifsupp.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
fvdifsupp.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
fvdifsupp.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) )
Assertion fvdifsupp ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 𝑍 )

Proof

Step Hyp Ref Expression
1 fvdifsupp.1 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2 fvdifsupp.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 fvdifsupp.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
4 fvdifsupp.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 ∖ ( 𝐹 supp 𝑍 ) ) )
5 4 eldifbd ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝐹 supp 𝑍 ) )
6 4 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
7 elsuppfn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) )
8 1 2 3 7 syl3anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) )
9 6 8 mpbirand ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) )
10 9 necon2bbid ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) = 𝑍 ↔ ¬ 𝑋 ∈ ( 𝐹 supp 𝑍 ) ) )
11 5 10 mpbird ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 𝑍 )