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 = I
Assertion rrxsca I V Scalar H = fld

Proof

Step Hyp Ref Expression
1 rrxsca.r H = I
2 eqid Base H = Base H
3 1 2 rrxprds I V H = toCPreHil fld 𝑠 I × subringAlg fld 𝑠 Base H
4 3 fveq2d I V Scalar H = Scalar toCPreHil fld 𝑠 I × subringAlg fld 𝑠 Base H
5 fvex Base fld 𝑠 I × subringAlg fld 𝑠 Base H V
6 5 mptex x Base fld 𝑠 I × subringAlg fld 𝑠 Base H x 𝑖 fld 𝑠 I × subringAlg fld 𝑠 Base H x V
7 eqid fld 𝑠 I × subringAlg fld 𝑠 Base H toNrmGrp x Base fld 𝑠 I × subringAlg fld 𝑠 Base H x 𝑖 fld 𝑠 I × subringAlg fld 𝑠 Base H x = fld 𝑠 I × subringAlg fld 𝑠 Base H toNrmGrp x Base fld 𝑠 I × subringAlg fld 𝑠 Base H x 𝑖 fld 𝑠 I × subringAlg fld 𝑠 Base H x
8 eqid Scalar fld 𝑠 I × subringAlg fld 𝑠 Base H = Scalar fld 𝑠 I × subringAlg fld 𝑠 Base H
9 7 8 tngsca x Base fld 𝑠 I × subringAlg fld 𝑠 Base H x 𝑖 fld 𝑠 I × subringAlg fld 𝑠 Base H x V Scalar fld 𝑠 I × subringAlg fld 𝑠 Base H = Scalar fld 𝑠 I × subringAlg fld 𝑠 Base H toNrmGrp x Base fld 𝑠 I × subringAlg fld 𝑠 Base H x 𝑖 fld 𝑠 I × subringAlg fld 𝑠 Base H x
10 9 eqcomd x Base fld 𝑠 I × subringAlg fld 𝑠 Base H x 𝑖 fld 𝑠 I × subringAlg fld 𝑠 Base H x V Scalar fld 𝑠 I × subringAlg fld 𝑠 Base H toNrmGrp x Base fld 𝑠 I × subringAlg fld 𝑠 Base H x 𝑖 fld 𝑠 I × subringAlg fld 𝑠 Base H x = Scalar fld 𝑠 I × subringAlg fld 𝑠 Base H
11 6 10 mp1i I V Scalar fld 𝑠 I × subringAlg fld 𝑠 Base H toNrmGrp x Base fld 𝑠 I × subringAlg fld 𝑠 Base H x 𝑖 fld 𝑠 I × subringAlg fld 𝑠 Base H x = Scalar fld 𝑠 I × subringAlg fld 𝑠 Base H
12 eqid toCPreHil fld 𝑠 I × subringAlg fld 𝑠 Base H = toCPreHil fld 𝑠 I × subringAlg fld 𝑠 Base H
13 eqid Base fld 𝑠 I × subringAlg fld 𝑠 Base H = Base fld 𝑠 I × subringAlg fld 𝑠 Base H
14 eqid 𝑖 fld 𝑠 I × subringAlg fld 𝑠 Base H = 𝑖 fld 𝑠 I × subringAlg fld 𝑠 Base H
15 12 13 14 tcphval toCPreHil fld 𝑠 I × subringAlg fld 𝑠 Base H = fld 𝑠 I × subringAlg fld 𝑠 Base H toNrmGrp x Base fld 𝑠 I × subringAlg fld 𝑠 Base H x 𝑖 fld 𝑠 I × subringAlg fld 𝑠 Base H x
16 15 fveq2i Scalar toCPreHil fld 𝑠 I × subringAlg fld 𝑠 Base H = Scalar fld 𝑠 I × subringAlg fld 𝑠 Base H toNrmGrp x Base fld 𝑠 I × subringAlg fld 𝑠 Base H x 𝑖 fld 𝑠 I × subringAlg fld 𝑠 Base H x
17 16 a1i I V Scalar toCPreHil fld 𝑠 I × subringAlg fld 𝑠 Base H = Scalar fld 𝑠 I × subringAlg fld 𝑠 Base H toNrmGrp x Base fld 𝑠 I × subringAlg fld 𝑠 Base H x 𝑖 fld 𝑠 I × subringAlg fld 𝑠 Base H x
18 eqid fld 𝑠 I × subringAlg fld = fld 𝑠 I × subringAlg fld
19 refld fld Field
20 19 a1i I V fld Field
21 id I V I V
22 snex subringAlg fld V
23 22 a1i I V subringAlg fld V
24 21 23 xpexd I V I × subringAlg fld V
25 18 20 24 prdssca I V fld = Scalar fld 𝑠 I × subringAlg fld
26 fvex Base H V
27 eqid fld 𝑠 I × subringAlg fld 𝑠 Base H = fld 𝑠 I × subringAlg fld 𝑠 Base H
28 eqid Scalar fld 𝑠 I × subringAlg fld = Scalar fld 𝑠 I × subringAlg fld
29 27 28 resssca Base H V Scalar fld 𝑠 I × subringAlg fld = Scalar fld 𝑠 I × subringAlg fld 𝑠 Base H
30 26 29 mp1i I V Scalar fld 𝑠 I × subringAlg fld = Scalar fld 𝑠 I × subringAlg fld 𝑠 Base H
31 25 30 eqtrd I V fld = Scalar fld 𝑠 I × subringAlg fld 𝑠 Base H
32 11 17 31 3eqtr4d I V Scalar toCPreHil fld 𝑠 I × subringAlg fld 𝑠 Base H = fld
33 4 32 eqtrd I V Scalar H = fld