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

Metamath Proof Explorer

Theorem suppssr

Description: A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 28-May-2019)

Ref Expression
Hypotheses suppssr.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
suppssr.n ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
suppssr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
suppssr.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
Assertion suppssr ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑍 )

Proof

Step Hyp Ref Expression
1 suppssr.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 suppssr.n ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
3 suppssr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 suppssr.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
5 eldif ⊢ ( 𝑋 ∈ ( 𝐴 ∖ 𝑊 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊 ) )
6 fvex ⊢ ( 𝐹 ‘ 𝑋 ) ∈ V
7 eldifsn ⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ ( V ∖ { 𝑍 } ) ↔ ( ( 𝐹 ‘ 𝑋 ) ∈ V ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) )
8 6 7 mpbiran ⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ ( V ∖ { 𝑍 } ) ↔ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 )
9 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
10 elsuppfn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝑈 ) → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) )
11 9 3 4 10 syl3anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) )
12 ibar ⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ V → ( ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ↔ ( ( 𝐹 ‘ 𝑋 ) ∈ V ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) )
13 6 12 mp1i ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ↔ ( ( 𝐹 ‘ 𝑋 ) ∈ V ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ) )
14 13 7 bitr4di ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ↔ ( 𝐹 ‘ 𝑋 ) ∈ ( V ∖ { 𝑍 } ) ) )
15 14 pm5.32da ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( V ∖ { 𝑍 } ) ) ) )
16 11 15 bitrd ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( V ∖ { 𝑍 } ) ) ) )
17 2 sseld ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp 𝑍 ) → 𝑋 ∈ 𝑊 ) )
18 16 17 sylbird ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( V ∖ { 𝑍 } ) ) → 𝑋 ∈ 𝑊 ) )
19 18 expdimp ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ ( V ∖ { 𝑍 } ) → 𝑋 ∈ 𝑊 ) )
20 8 19 biimtrrid ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑋 ) ≠ 𝑍 → 𝑋 ∈ 𝑊 ) )
21 20 necon1bd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐴 ) → ( ¬ 𝑋 ∈ 𝑊 → ( 𝐹 ‘ 𝑋 ) = 𝑍 ) )
22 21 impr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐴 ∧ ¬ 𝑋 ∈ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑍 )
23 5 22 sylan2b ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑍 )