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 eqtrdi 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