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 = ( RR^ ` I )
Assertion rrxsca 
|- ( I e. V -> ( Scalar ` H ) = RRfld )

Proof

Step Hyp Ref Expression
1 rrxsca.r 
 |-  H = ( RR^ ` I )
2 eqid 
 |-  ( Base ` H ) = ( Base ` H )
3 1 2 rrxprds 
 |-  ( I e. V -> H = ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) )
4 3 fveq2d 
 |-  ( I e. V -> ( Scalar ` H ) = ( Scalar ` ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) ) )
5 fvex 
 |-  ( Base ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) e. _V
6 5 mptex 
 |-  ( x e. ( Base ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) |-> ( sqrt ` ( x ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) x ) ) ) e. _V
7 eqid 
 |-  ( ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) toNrmGrp ( x e. ( Base ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) |-> ( sqrt ` ( x ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) x ) ) ) ) = ( ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) toNrmGrp ( x e. ( Base ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) |-> ( sqrt ` ( x ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) x ) ) ) )
8 eqid 
 |-  ( Scalar ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) = ( Scalar ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) )
9 7 8 tngsca 
 |-  ( ( x e. ( Base ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) |-> ( sqrt ` ( x ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) x ) ) ) e. _V -> ( Scalar ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) = ( Scalar ` ( ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) toNrmGrp ( x e. ( Base ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) |-> ( sqrt ` ( x ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) x ) ) ) ) ) )
10 9 eqcomd 
 |-  ( ( x e. ( Base ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) |-> ( sqrt ` ( x ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) x ) ) ) e. _V -> ( Scalar ` ( ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) toNrmGrp ( x e. ( Base ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) |-> ( sqrt ` ( x ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) x ) ) ) ) ) = ( Scalar ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) )
11 6 10 mp1i 
 |-  ( I e. V -> ( Scalar ` ( ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) toNrmGrp ( x e. ( Base ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) |-> ( sqrt ` ( x ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) x ) ) ) ) ) = ( Scalar ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) )
12 eqid 
 |-  ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) = ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) )
13 eqid 
 |-  ( Base ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) = ( Base ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) )
14 eqid 
 |-  ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) = ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) )
15 12 13 14 tcphval 
 |-  ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) = ( ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) toNrmGrp ( x e. ( Base ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) |-> ( sqrt ` ( x ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) x ) ) ) )
16 15 fveq2i 
 |-  ( Scalar ` ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) ) = ( Scalar ` ( ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) toNrmGrp ( x e. ( Base ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) |-> ( sqrt ` ( x ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) x ) ) ) ) )
17 16 a1i 
 |-  ( I e. V -> ( Scalar ` ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) ) = ( Scalar ` ( ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) toNrmGrp ( x e. ( Base ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) |-> ( sqrt ` ( x ( .i ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) x ) ) ) ) ) )
18 eqid 
 |-  ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) = ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) )
19 refld 
 |-  RRfld e. Field
20 19 a1i 
 |-  ( I e. V -> RRfld e. Field )
21 id 
 |-  ( I e. V -> I e. V )
22 snex 
 |-  { ( ( subringAlg ` RRfld ) ` RR ) } e. _V
23 22 a1i 
 |-  ( I e. V -> { ( ( subringAlg ` RRfld ) ` RR ) } e. _V )
24 21 23 xpexd 
 |-  ( I e. V -> ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) e. _V )
25 18 20 24 prdssca 
 |-  ( I e. V -> RRfld = ( Scalar ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) )
26 fvex 
 |-  ( Base ` H ) e. _V
27 eqid 
 |-  ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) = ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) )
28 eqid 
 |-  ( Scalar ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) = ( Scalar ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) )
29 27 28 resssca 
 |-  ( ( Base ` H ) e. _V -> ( Scalar ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) = ( Scalar ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) )
30 26 29 mp1i 
 |-  ( I e. V -> ( Scalar ` ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) ) = ( Scalar ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) )
31 25 30 eqtrd 
 |-  ( I e. V -> RRfld = ( Scalar ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) )
32 11 17 31 3eqtr4d 
 |-  ( I e. V -> ( Scalar ` ( toCPreHil ` ( ( RRfld Xs_ ( I X. { ( ( subringAlg ` RRfld ) ` RR ) } ) ) |`s ( Base ` H ) ) ) ) = RRfld )
33 4 32 eqtrd 
 |-  ( I e. V -> ( Scalar ` H ) = RRfld )