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 ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
Assertion rrxsca ( 𝐼 ∈ 𝑉 → ( Scalar ‘ 𝐻 ) = ℝfld )

Proof

Step Hyp Ref Expression
1 rrxsca.r ⊢ 𝐻 = ( ℝ^ ‘ 𝐼 )
2 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
3 1 2 rrxprds ⊢ ( 𝐼 ∈ 𝑉 → 𝐻 = ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) )
4 3 fveq2d ⊢ ( 𝐼 ∈ 𝑉 → ( Scalar ‘ 𝐻 ) = ( Scalar ‘ ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ) )
5 fvex ⊢ ( Base ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ∈ V
6 5 mptex ⊢ ( 𝑥 ∈ ( Base ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) 𝑥 ) ) ) ∈ V
7 eqid ⊢ ( ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) 𝑥 ) ) ) ) = ( ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) 𝑥 ) ) ) )
8 eqid ⊢ ( Scalar ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) = ( Scalar ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) )
9 7 8 tngsca ⊢ ( ( 𝑥 ∈ ( Base ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) 𝑥 ) ) ) ∈ V → ( Scalar ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) = ( Scalar ‘ ( ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) 𝑥 ) ) ) ) ) )
10 9 eqcomd ⊢ ( ( 𝑥 ∈ ( Base ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) 𝑥 ) ) ) ∈ V → ( Scalar ‘ ( ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) 𝑥 ) ) ) ) ) = ( Scalar ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) )
11 6 10 mp1i ⊢ ( 𝐼 ∈ 𝑉 → ( Scalar ‘ ( ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) 𝑥 ) ) ) ) ) = ( Scalar ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) )
12 eqid ⊢ ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) = ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) )
13 eqid ⊢ ( Base ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) = ( Base ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) )
14 eqid ⊢ ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) = ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) )
15 12 13 14 tcphval ⊢ ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) = ( ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) 𝑥 ) ) ) )
16 15 fveq2i ⊢ ( Scalar ‘ ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ) = ( Scalar ‘ ( ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) 𝑥 ) ) ) ) )
17 16 a1i ⊢ ( 𝐼 ∈ 𝑉 → ( Scalar ‘ ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ) = ( Scalar ‘ ( ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) toNrmGrp ( 𝑥 ∈ ( Base ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) 𝑥 ) ) ) ) ) )
18 eqid ⊢ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) = ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) )
19 refld ⊢ ℝfld ∈ Field
20 19 a1i ⊢ ( 𝐼 ∈ 𝑉 → ℝfld ∈ Field )
21 id ⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉 )
22 snex ⊢ { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ∈ V
23 22 a1i ⊢ ( 𝐼 ∈ 𝑉 → { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ∈ V )
24 21 23 xpexd ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ∈ V )
25 18 20 24 prdssca ⊢ ( 𝐼 ∈ 𝑉 → ℝfld = ( Scalar ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) )
26 fvex ⊢ ( Base ‘ 𝐻 ) ∈ V
27 eqid ⊢ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) = ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) )
28 eqid ⊢ ( Scalar ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) = ( Scalar ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) )
29 27 28 resssca ⊢ ( ( Base ‘ 𝐻 ) ∈ V → ( Scalar ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) = ( Scalar ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) )
30 26 29 mp1i ⊢ ( 𝐼 ∈ 𝑉 → ( Scalar ‘ ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ) = ( Scalar ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) )
31 25 30 eqtrd ⊢ ( 𝐼 ∈ 𝑉 → ℝfld = ( Scalar ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) )
32 11 17 31 3eqtr4d ⊢ ( 𝐼 ∈ 𝑉 → ( Scalar ‘ ( toℂPreHil ‘ ( ( ℝfld Xs ( 𝐼 × { ( ( subringAlg ‘ ℝfld ) ‘ ℝ ) } ) ) ↾s ( Base ‘ 𝐻 ) ) ) ) = ℝfld )
33 4 32 eqtrd ⊢ ( 𝐼 ∈ 𝑉 → ( Scalar ‘ 𝐻 ) = ℝfld )