Metamath Proof Explorer

Theorem fdifsuppconst

Description: A function is a zero constant outside of its support. (Contributed by Thierry Arnoux, 22-Jun-2024)

Ref Expression
Hypothesis fdifsuppconst.1 ⊢ A = dom ⁡ F ∖ supp Z⁡ F
Assertion fdifsuppconst ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → F ↾ A = A × Z

Proof

Step Hyp Ref Expression
1 fdifsuppconst.1 ⊢ A = dom ⁡ F ∖ supp Z⁡ F
2 funfn ⊢ Fun ⁡ F ↔ F Fn dom ⁡ F
3 2 biimpi ⊢ Fun ⁡ F → F Fn dom ⁡ F
4 3 ad2antrr ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → F Fn dom ⁡ F
5 difssd ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → dom ⁡ F ∖ supp Z⁡ F ⊆ dom ⁡ F
6 1 5 eqsstrid ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → A ⊆ dom ⁡ F
7 4 6 fnssresd ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → F ↾ A Fn A
8 fnconstg ⊢ Z ∈ W → A × Z Fn A
9 8 adantl ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → A × Z Fn A
10 4 adantr ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W ∧ x ∈ A → F Fn dom ⁡ F
11 dmexg ⊢ F ∈ V → dom ⁡ F ∈ V
12 11 ad3antlr ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W ∧ x ∈ A → dom ⁡ F ∈ V
13 simplr ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W ∧ x ∈ A → Z ∈ W
14 1 eleq2i ⊢ x ∈ A ↔ x ∈ dom ⁡ F ∖ supp Z⁡ F
15 14 biimpi ⊢ x ∈ A → x ∈ dom ⁡ F ∖ supp Z⁡ F
16 15 adantl ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W ∧ x ∈ A → x ∈ dom ⁡ F ∖ supp Z⁡ F
17 10 12 13 16 fvdifsupp ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W ∧ x ∈ A → F ⁡ x = Z
18 simpr ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W ∧ x ∈ A → x ∈ A
19 18 fvresd ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W ∧ x ∈ A → F ↾ A ⁡ x = F ⁡ x
20 fvconst2g ⊢ Z ∈ W ∧ x ∈ A → A × Z ⁡ x = Z
21 20 adantll ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W ∧ x ∈ A → A × Z ⁡ x = Z
22 17 19 21 3eqtr4d ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W ∧ x ∈ A → F ↾ A ⁡ x = A × Z ⁡ x
23 7 9 22 eqfnfvd ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → F ↾ A = A × Z
24 23 3impa ⊢ Fun ⁡ F ∧ F ∈ V ∧ Z ∈ W → F ↾ A = A × Z