Metamath Proof Explorer


Theorem rrxsca

Description: The field of real numbers is the scalar field of the generalized real Euclidean space. (Contributed by AV, 15-Jan-2023)

Ref Expression
Hypothesis rrxsca.r H=msup
Assertion rrxsca IVScalarH=fld

Proof

Step Hyp Ref Expression
1 rrxsca.r H=msup
2 eqid BaseH=BaseH
3 1 2 rrxprds IVH=toCPreHilfld𝑠I×subringAlgfld𝑠BaseH
4 3 fveq2d IVScalarH=ScalartoCPreHilfld𝑠I×subringAlgfld𝑠BaseH
5 fvex Basefld𝑠I×subringAlgfld𝑠BaseHV
6 5 mptex xBasefld𝑠I×subringAlgfld𝑠BaseHx𝑖fld𝑠I×subringAlgfld𝑠BaseHxV
7 eqid fld𝑠I×subringAlgfld𝑠BaseHtoNrmGrpxBasefld𝑠I×subringAlgfld𝑠BaseHx𝑖fld𝑠I×subringAlgfld𝑠BaseHx=fld𝑠I×subringAlgfld𝑠BaseHtoNrmGrpxBasefld𝑠I×subringAlgfld𝑠BaseHx𝑖fld𝑠I×subringAlgfld𝑠BaseHx
8 eqid Scalarfld𝑠I×subringAlgfld𝑠BaseH=Scalarfld𝑠I×subringAlgfld𝑠BaseH
9 7 8 tngsca xBasefld𝑠I×subringAlgfld𝑠BaseHx𝑖fld𝑠I×subringAlgfld𝑠BaseHxVScalarfld𝑠I×subringAlgfld𝑠BaseH=Scalarfld𝑠I×subringAlgfld𝑠BaseHtoNrmGrpxBasefld𝑠I×subringAlgfld𝑠BaseHx𝑖fld𝑠I×subringAlgfld𝑠BaseHx
10 9 eqcomd xBasefld𝑠I×subringAlgfld𝑠BaseHx𝑖fld𝑠I×subringAlgfld𝑠BaseHxVScalarfld𝑠I×subringAlgfld𝑠BaseHtoNrmGrpxBasefld𝑠I×subringAlgfld𝑠BaseHx𝑖fld𝑠I×subringAlgfld𝑠BaseHx=Scalarfld𝑠I×subringAlgfld𝑠BaseH
11 6 10 mp1i IVScalarfld𝑠I×subringAlgfld𝑠BaseHtoNrmGrpxBasefld𝑠I×subringAlgfld𝑠BaseHx𝑖fld𝑠I×subringAlgfld𝑠BaseHx=Scalarfld𝑠I×subringAlgfld𝑠BaseH
12 eqid toCPreHilfld𝑠I×subringAlgfld𝑠BaseH=toCPreHilfld𝑠I×subringAlgfld𝑠BaseH
13 eqid Basefld𝑠I×subringAlgfld𝑠BaseH=Basefld𝑠I×subringAlgfld𝑠BaseH
14 eqid 𝑖fld𝑠I×subringAlgfld𝑠BaseH=𝑖fld𝑠I×subringAlgfld𝑠BaseH
15 12 13 14 tcphval toCPreHilfld𝑠I×subringAlgfld𝑠BaseH=fld𝑠I×subringAlgfld𝑠BaseHtoNrmGrpxBasefld𝑠I×subringAlgfld𝑠BaseHx𝑖fld𝑠I×subringAlgfld𝑠BaseHx
16 15 fveq2i ScalartoCPreHilfld𝑠I×subringAlgfld𝑠BaseH=Scalarfld𝑠I×subringAlgfld𝑠BaseHtoNrmGrpxBasefld𝑠I×subringAlgfld𝑠BaseHx𝑖fld𝑠I×subringAlgfld𝑠BaseHx
17 16 a1i IVScalartoCPreHilfld𝑠I×subringAlgfld𝑠BaseH=Scalarfld𝑠I×subringAlgfld𝑠BaseHtoNrmGrpxBasefld𝑠I×subringAlgfld𝑠BaseHx𝑖fld𝑠I×subringAlgfld𝑠BaseHx
18 eqid fld𝑠I×subringAlgfld=fld𝑠I×subringAlgfld
19 refld fldField
20 19 a1i IVfldField
21 id IVIV
22 snex subringAlgfldV
23 22 a1i IVsubringAlgfldV
24 21 23 xpexd IVI×subringAlgfldV
25 18 20 24 prdssca IVfld=Scalarfld𝑠I×subringAlgfld
26 fvex BaseHV
27 eqid fld𝑠I×subringAlgfld𝑠BaseH=fld𝑠I×subringAlgfld𝑠BaseH
28 eqid Scalarfld𝑠I×subringAlgfld=Scalarfld𝑠I×subringAlgfld
29 27 28 resssca BaseHVScalarfld𝑠I×subringAlgfld=Scalarfld𝑠I×subringAlgfld𝑠BaseH
30 26 29 mp1i IVScalarfld𝑠I×subringAlgfld=Scalarfld𝑠I×subringAlgfld𝑠BaseH
31 25 30 eqtrd IVfld=Scalarfld𝑠I×subringAlgfld𝑠BaseH
32 11 17 31 3eqtr4d IVScalartoCPreHilfld𝑠I×subringAlgfld𝑠BaseH=fld
33 4 32 eqtrd IVScalarH=fld