Theorem fsuppssindlem1

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

	Ref	Expression
Hypotheses	fsuppssindlem1.z	$$⊢\phi \to \underset{\dot{}}{0}\in W$$
	fsuppssindlem1.v	$$⊢\phi \to I\in V$$
	fsuppssindlem1.1	$$⊢\phi \to F:I⟶B$$
	fsuppssindlem1.2	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{0}\subseteq S$$
Assertion	fsuppssindlem1	$$⊢\phi \to F=\left(x\in I⟼if\left(x\in S,\left({F\upharpoonright }_S\right)\left(x\right),\underset{\dot{}}{0}\right)\right)$$

Proof

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