Theorem rrxbase

Description: The base of the generalized real Euclidean space is the set of functions with finite support. (Contributed by Thierry Arnoux, 16-Jun-2019) (Proof shortened by AV, 22-Jul-2019)

	Ref	Expression
Hypotheses	rrxval.r
	rrxbase.b	$$⊢B={\mathrm{Base}}_H$$
Assertion	rrxbase	$$⊢I\in V\to B=\left\{f\in \left({ℝ}^I\right)|{finSupp}_0\left(f\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rrxval.r
2		rrxbase.b	$$⊢B={\mathrm{Base}}_H$$
3	1	rrxval	$$⊢I\in V\to H=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
4	3	fveq2d	$$⊢I\in V\to {\mathrm{Base}}_H={\mathrm{Base}}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
5		eqid	$$⊢\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
6		eqid	$$⊢{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
7	5 6	tcphbas	$$⊢{\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}={\mathrm{Base}}_{\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
8	4 7	syl6eqr	$$⊢I\in V\to {\mathrm{Base}}_H={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
9	2	a1i	$$⊢I\in V\to B={\mathrm{Base}}_H$$
10		refld	$$⊢{ℝ}_{\mathrm{fld}}\in \mathrm{Field}$$
11		eqid	$$⊢{ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I={ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I$$
12		rebase	$$⊢ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$$
13		re0g	$$⊢0=0_{{ℝ}_{\mathrm{fld}}}$$
14		eqid	$$⊢\left\{f\in \left({ℝ}^I\right)|{finSupp}_0\left(f\right)\right\}=\left\{f\in \left({ℝ}^I\right)|{finSupp}_0\left(f\right)\right\}$$
15	11 12 13 14	frlmbas	$$⊢\left({ℝ}_{\mathrm{fld}}\in \mathrm{Field}\wedge I\in V\right)\to \left\{f\in \left({ℝ}^I\right)|{finSupp}_0\left(f\right)\right\}={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
16	10 15	mpan	$$⊢I\in V\to \left\{f\in \left({ℝ}^I\right)|{finSupp}_0\left(f\right)\right\}={\mathrm{Base}}_{\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)}$$
17	8 9 16	3eqtr4d	$$⊢I\in V\to B=\left\{f\in \left({ℝ}^I\right)|{finSupp}_0\left(f\right)\right\}$$