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