Theorem rrxfsupp

Description: Euclidean vectors are of finite support. (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	rrxfsupp	$$⊢\phi \to F\mathrm{supp}0\in \mathrm{Fin}$$

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	2 1	eleqtrdi	$$⊢\phi \to F\in \left\{h\in \left({ℝ}^I\right)|{finSupp}_0\left(h\right)\right\}$$
4		breq1	$$⊢h=F\to \left({finSupp}_0\left(h\right)\leftrightarrow {finSupp}_0\left(F\right)\right)$$
5	4	elrab	$$⊢F\in \left\{h\in \left({ℝ}^I\right)|{finSupp}_0\left(h\right)\right\}\leftrightarrow \left(F\in \left({ℝ}^I\right)\wedge {finSupp}_0\left(F\right)\right)$$
6	3 5	sylib	$$⊢\phi \to \left(F\in \left({ℝ}^I\right)\wedge {finSupp}_0\left(F\right)\right)$$
7	6	simprd	$$⊢\phi \to {finSupp}_0\left(F\right)$$
8	7	fsuppimpd	$$⊢\phi \to F\mathrm{supp}0\in \mathrm{Fin}$$