Theorem rrxsuppss

Description: Support of Euclidean vectors. (Contributed by Thierry Arnoux, 7-Jul-2019)

	Ref	Expression
Hypotheses	rrxmval.1	$$⊢X=\left\{h\in \left({ℝ}^I\right)|{finSupp}_0\left(h\right)\right\}$$
	rrxf.1	$$⊢\phi \to F\in X$$
Assertion	rrxsuppss	$$⊢\phi \to F\mathrm{supp}0\subseteq I$$

Proof

Step	Hyp	Ref	Expression
1		rrxmval.1	$$⊢X=\left\{h\in \left({ℝ}^I\right)|{finSupp}_0\left(h\right)\right\}$$
2		rrxf.1	$$⊢\phi \to F\in X$$
3		suppssdm	$$⊢F\mathrm{supp}0\subseteq \mathrm{dom}F$$
4	1 2	rrxf	$$⊢\phi \to F:I⟶ℝ$$
5	3 4	fssdm	$$⊢\phi \to F\mathrm{supp}0\subseteq I$$