Theorem rrxval

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

	Ref	Expression
Hypothesis	rrxval.r	⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
Assertion	rrxval	⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrxval.r	⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
2		elex	⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ V )
3		oveq2	⊢ ( 𝑖 = 𝐼 → ( ℝfld freeLMod 𝑖 ) = ( ℝfld freeLMod 𝐼 ) )
4	3	fveq2d	⊢ ( 𝑖 = 𝐼 → ( toℂPreHil ‘ ( ℝfld freeLMod 𝑖 ) ) = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
5		df-rrx	⊢ ℝ^ = ( 𝑖 ∈ V ↦ ( toℂPreHil ‘ ( ℝfld freeLMod 𝑖 ) ) )
6		fvex	⊢ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ∈ V
7	4 5 6	fvmpt	⊢ ( 𝐼 ∈ V → ( ℝ^ ‘ 𝐼 ) = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
8	2 7	syl	⊢ ( 𝐼 ∈ 𝑉 → ( ℝ^ ‘ 𝐼 ) = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
9	1 8	syl5eq	⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )