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 ⊢ H = I
Assertion rrxval ⊢ I ∈ V → H = toCPreHil ⁡ ℝ fld freeLMod I

Proof

Step Hyp Ref Expression
1 rrxval.r ⊢ H = I
2 elex ⊢ I ∈ V → I ∈ V
3 oveq2 ⊢ i = I → ℝ fld freeLMod i = ℝ fld freeLMod I
4 3 fveq2d ⊢ i = I → toCPreHil ⁡ ℝ fld freeLMod i = toCPreHil ⁡ ℝ fld freeLMod I
5 df-rrx ⊢ ℝ↑ = i ∈ V ⟼ toCPreHil ⁡ ℝ fld freeLMod i
6 fvex ⊢ toCPreHil ⁡ ℝ fld freeLMod I ∈ V
7 4 5 6 fvmpt ⊢ I ∈ V → I = toCPreHil ⁡ ℝ fld freeLMod I
8 2 7 syl ⊢ I ∈ V → I = toCPreHil ⁡ ℝ fld freeLMod I
9 1 8 eqtrid ⊢ I ∈ V → H = toCPreHil ⁡ ℝ fld freeLMod I