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 )