fsuppssindlem1

Description: Lemma for fsuppssind . Functions are zero outside of their support. (Contributed by SN, 15-Jul-2024)

	Ref	Expression
Hypotheses	fsuppssindlem1.z	$⊢ φ \to \underset{˙}{0} \in W$
	fsuppssindlem1.v	$⊢ φ \to I \in V$
	fsuppssindlem1.1	$⊢ φ \to F : I ⟶ B$
	fsuppssindlem1.2	$⊢ φ \to F supp \underset{˙}{0} \subseteq S$
Assertion	fsuppssindlem1	$⊢ φ \to F = (x \in I ⟼ if (x \in S, ({F ↾}_{S}) (x), \underset{˙}{0}))$

Step	Hyp	Ref	Expression
1		fsuppssindlem1.z	$⊢ φ \to \underset{˙}{0} \in W$
2		fsuppssindlem1.v	$⊢ φ \to I \in V$
3		fsuppssindlem1.1	$⊢ φ \to F : I ⟶ B$
4		fsuppssindlem1.2	$⊢ φ \to F supp \underset{˙}{0} \subseteq S$
5	3	feqmptd	$⊢ φ \to F = (x \in I ⟼ F (x))$
6		fvres	$⊢ x \in S \to ({F ↾}_{S}) (x) = F (x)$
7	6	adantl	$⊢ ((φ \land x \in I) \land x \in S) \to ({F ↾}_{S}) (x) = F (x)$
8		eldif	$⊢ x \in (I ∖ S) \leftrightarrow (x \in I \land \neg x \in S)$
9	3 4 2 1	suppssr	$⊢ (φ \land x \in (I ∖ S)) \to F (x) = \underset{˙}{0}$
10	9	eqcomd	$⊢ (φ \land x \in (I ∖ S)) \to \underset{˙}{0} = F (x)$
11	8 10	sylan2br	$⊢ (φ \land (x \in I \land \neg x \in S)) \to \underset{˙}{0} = F (x)$
12	11	anassrs	$⊢ ((φ \land x \in I) \land \neg x \in S) \to \underset{˙}{0} = F (x)$
13	7 12	ifeqda	$⊢ (φ \land x \in I) \to if (x \in S, ({F ↾}_{S}) (x), \underset{˙}{0}) = F (x)$
14	13	mpteq2dva	$⊢ φ \to (x \in I ⟼ if (x \in S, ({F ↾}_{S}) (x), \underset{˙}{0})) = (x \in I ⟼ F (x))$
15	5 14	eqtr4d	$⊢ φ \to F = (x \in I ⟼ if (x \in S, ({F ↾}_{S}) (x), \underset{˙}{0}))$

Metamath Proof Explorer