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 \land F \in V \land Z \in W) \to {F ↾}_{A} = A \times \{Z\}$

Proof

Step	Hyp	Ref	Expression
1		fdifsuppconst.1	$⊢ A = dom F ∖ {supp}_{Z} (F)$
2		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
3	2	biimpi	$⊢ Fun F \to F Fn dom F$
4	3	ad2antrr	$⊢ ((Fun F \land F \in V) \land Z \in W) \to F Fn dom F$
5		difssd	$⊢ ((Fun F \land F \in V) \land Z \in W) \to dom F ∖ {supp}_{Z} (F) \subseteq dom F$
6	1 5	eqsstrid	$⊢ ((Fun F \land F \in V) \land Z \in W) \to A \subseteq dom F$
7	4 6	fnssresd	$⊢ ((Fun F \land F \in V) \land Z \in W) \to ({F ↾}_{A}) Fn A$
8		fnconstg	$⊢ Z \in W \to (A \times \{Z\}) Fn A$
9	8	adantl	$⊢ ((Fun F \land F \in V) \land Z \in W) \to (A \times \{Z\}) Fn A$
10	4	adantr	$⊢ (((Fun F \land F \in V) \land Z \in W) \land x \in A) \to F Fn dom F$
11		dmexg	$⊢ F \in V \to dom F \in V$
12	11	ad3antlr	$⊢ (((Fun F \land F \in V) \land Z \in W) \land x \in A) \to dom F \in V$
13		simplr	$⊢ (((Fun F \land F \in V) \land Z \in W) \land x \in A) \to Z \in W$
14	1	eleq2i	$⊢ x \in A \leftrightarrow x \in (dom F ∖ {supp}_{Z} (F))$
15	14	biimpi	$⊢ x \in A \to x \in (dom F ∖ {supp}_{Z} (F))$
16	15	adantl	$⊢ (((Fun F \land F \in V) \land Z \in W) \land x \in A) \to x \in (dom F ∖ {supp}_{Z} (F))$
17	10 12 13 16	fvdifsupp	$⊢ (((Fun F \land F \in V) \land Z \in W) \land x \in A) \to F (x) = Z$
18		simpr	$⊢ (((Fun F \land F \in V) \land Z \in W) \land x \in A) \to x \in A$
19	18	fvresd	$⊢ (((Fun F \land F \in V) \land Z \in W) \land x \in A) \to ({F ↾}_{A}) (x) = F (x)$
20		fvconst2g	$⊢ (Z \in W \land x \in A) \to (A \times \{Z\}) (x) = Z$
21	20	adantll	$⊢ (((Fun F \land F \in V) \land Z \in W) \land x \in A) \to (A \times \{Z\}) (x) = Z$
22	17 19 21	3eqtr4d	$⊢ (((Fun F \land F \in V) \land Z \in W) \land x \in A) \to ({F ↾}_{A}) (x) = (A \times \{Z\}) (x)$
23	7 9 22	eqfnfvd	$⊢ ((Fun F \land F \in V) \land Z \in W) \to {F ↾}_{A} = A \times \{Z\}$
24	23	3impa	$⊢ (Fun F \land F \in V \land Z \in W) \to {F ↾}_{A} = A \times \{Z\}$

Metamath Proof Explorer

Theorem fdifsuppconst

Proof