Theorem rrxval

Description: Value of the generalized Euclidean space. (Contributed by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Hypothesis	rrxval.r
Assertion	rrxval	$$⊢I\in V\to H=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$

Proof

Step	Hyp	Ref	Expression
1		rrxval.r
2		elex	$$⊢I\in V\to I\in \mathrm{V}$$
3		oveq2	$$⊢i=I\to {ℝ}_{\mathrm{fld}}\mathrm{freeLMod}i={ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I$$
4	3	fveq2d	$$⊢i=I\to \mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}i\right)=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$
5		df-rrx	$$⊢\mathrm{ℝ\uparrow }=\left(i\in \mathrm{V}⟼\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}i\right)\right)$$
6		fvex	$$⊢\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)\in \mathrm{V}$$
7	4 5 6	fvmpt
8	2 7	syl
9	1 8	syl5eq	$$⊢I\in V\to H=\mathrm{toCPreHil}\left({ℝ}_{\mathrm{fld}}\mathrm{freeLMod}I\right)$$