Metamath Proof Explorer

Theorem rrxdim

Description: Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023)

Ref Expression
Hypothesis rrxdim.1 ⊢ H = I
Assertion rrxdim ⊢ I ∈ V → dim ⁡ H = I

Proof

Step Hyp Ref Expression
1 rrxdim.1 ⊢ H = I
2 1 rrxval ⊢ I ∈ V → H = toCPreHil ⁡ ℝ fld freeLMod I
3 eqid ⊢ toCPreHil ⁡ ℝ fld freeLMod I = toCPreHil ⁡ ℝ fld freeLMod I
4 eqid ⊢ Base ℝ fld freeLMod I = Base ℝ fld freeLMod I
5 eqid ⊢ ⋅ 𝑖 ⁡ ℝ fld freeLMod I = ⋅ 𝑖 ⁡ ℝ fld freeLMod I
6 3 4 5 tcphval ⊢ toCPreHil ⁡ ℝ fld freeLMod I = ℝ fld freeLMod I toNrmGrp x ∈ Base ℝ fld freeLMod I ⟼ x ⋅ 𝑖 ⁡ ℝ fld freeLMod I x
7 2 6 syl6eq ⊢ I ∈ V → H = ℝ fld freeLMod I toNrmGrp x ∈ Base ℝ fld freeLMod I ⟼ x ⋅ 𝑖 ⁡ ℝ fld freeLMod I x
8 7 fveq2d ⊢ I ∈ V → dim ⁡ H = dim ⁡ ℝ fld freeLMod I toNrmGrp x ∈ Base ℝ fld freeLMod I ⟼ x ⋅ 𝑖 ⁡ ℝ fld freeLMod I x
9 resubdrg ⊢ ℝ ∈ SubRing ⁡ ℂ fld ∧ ℝ fld ∈ DivRing
10 9 simpri ⊢ ℝ fld ∈ DivRing
11 eqid ⊢ ℝ fld freeLMod I = ℝ fld freeLMod I
12 11 frlmlvec ⊢ ℝ fld ∈ DivRing ∧ I ∈ V → ℝ fld freeLMod I ∈ LVec
13 10 12 mpan ⊢ I ∈ V → ℝ fld freeLMod I ∈ LVec
14 4 tcphex ⊢ x ∈ Base ℝ fld freeLMod I ⟼ x ⋅ 𝑖 ⁡ ℝ fld freeLMod I x ∈ V
15 eqid ⊢ ℝ fld freeLMod I toNrmGrp x ∈ Base ℝ fld freeLMod I ⟼ x ⋅ 𝑖 ⁡ ℝ fld freeLMod I x = ℝ fld freeLMod I toNrmGrp x ∈ Base ℝ fld freeLMod I ⟼ x ⋅ 𝑖 ⁡ ℝ fld freeLMod I x
16 15 tngdim ⊢ ℝ fld freeLMod I ∈ LVec ∧ x ∈ Base ℝ fld freeLMod I ⟼ x ⋅ 𝑖 ⁡ ℝ fld freeLMod I x ∈ V → dim ⁡ ℝ fld freeLMod I = dim ⁡ ℝ fld freeLMod I toNrmGrp x ∈ Base ℝ fld freeLMod I ⟼ x ⋅ 𝑖 ⁡ ℝ fld freeLMod I x
17 13 14 16 sylancl ⊢ I ∈ V → dim ⁡ ℝ fld freeLMod I = dim ⁡ ℝ fld freeLMod I toNrmGrp x ∈ Base ℝ fld freeLMod I ⟼ x ⋅ 𝑖 ⁡ ℝ fld freeLMod I x
18 11 frlmdim ⊢ ℝ fld ∈ DivRing ∧ I ∈ V → dim ⁡ ℝ fld freeLMod I = I
19 10 18 mpan ⊢ I ∈ V → dim ⁡ ℝ fld freeLMod I = I
20 8 17 19 3eqtr2d ⊢ I ∈ V → dim ⁡ H = I