This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )