Metamath Proof Explorer

Theorem rrxdim

Description: Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023)

Ref Expression
Hypothesis rrxdim.1 
|- H = ( RR^ ` I )
Assertion rrxdim 
|- ( I e. V -> ( dim ` H ) = ( # ` I ) )

Proof

Step Hyp Ref Expression
1 rrxdim.1 
 |-  H = ( RR^ ` I )
2 1 rrxval 
 |-  ( I e. V -> H = ( toCPreHil ` ( RRfld freeLMod I ) ) )
3 eqid 
 |-  ( toCPreHil ` ( RRfld freeLMod I ) ) = ( toCPreHil ` ( RRfld freeLMod I ) )
4 eqid 
 |-  ( Base ` ( RRfld freeLMod I ) ) = ( Base ` ( RRfld freeLMod I ) )
5 eqid 
 |-  ( .i ` ( RRfld freeLMod I ) ) = ( .i ` ( RRfld freeLMod I ) )
6 3 4 5 tcphval 
 |-  ( toCPreHil ` ( RRfld freeLMod I ) ) = ( ( RRfld freeLMod I ) toNrmGrp ( x e. ( Base ` ( RRfld freeLMod I ) ) |-> ( sqrt ` ( x ( .i ` ( RRfld freeLMod I ) ) x ) ) ) )
7 2 6 eqtrdi 
 |-  ( I e. V -> H = ( ( RRfld freeLMod I ) toNrmGrp ( x e. ( Base ` ( RRfld freeLMod I ) ) |-> ( sqrt ` ( x ( .i ` ( RRfld freeLMod I ) ) x ) ) ) ) )
8 7 fveq2d 
 |-  ( I e. V -> ( dim ` H ) = ( dim ` ( ( RRfld freeLMod I ) toNrmGrp ( x e. ( Base ` ( RRfld freeLMod I ) ) |-> ( sqrt ` ( x ( .i ` ( RRfld freeLMod I ) ) x ) ) ) ) ) )
9 resubdrg 
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
10 9 simpri 
 |-  RRfld e. DivRing
11 eqid 
 |-  ( RRfld freeLMod I ) = ( RRfld freeLMod I )
12 11 frlmlvec 
 |-  ( ( RRfld e. DivRing /\ I e. V ) -> ( RRfld freeLMod I ) e. LVec )
13 10 12 mpan 
 |-  ( I e. V -> ( RRfld freeLMod I ) e. LVec )
14 4 tcphex 
 |-  ( x e. ( Base ` ( RRfld freeLMod I ) ) |-> ( sqrt ` ( x ( .i ` ( RRfld freeLMod I ) ) x ) ) ) e. _V
15 eqid 
 |-  ( ( RRfld freeLMod I ) toNrmGrp ( x e. ( Base ` ( RRfld freeLMod I ) ) |-> ( sqrt ` ( x ( .i ` ( RRfld freeLMod I ) ) x ) ) ) ) = ( ( RRfld freeLMod I ) toNrmGrp ( x e. ( Base ` ( RRfld freeLMod I ) ) |-> ( sqrt ` ( x ( .i ` ( RRfld freeLMod I ) ) x ) ) ) )
16 15 tngdim 
 |-  ( ( ( RRfld freeLMod I ) e. LVec /\ ( x e. ( Base ` ( RRfld freeLMod I ) ) |-> ( sqrt ` ( x ( .i ` ( RRfld freeLMod I ) ) x ) ) ) e. _V ) -> ( dim ` ( RRfld freeLMod I ) ) = ( dim ` ( ( RRfld freeLMod I ) toNrmGrp ( x e. ( Base ` ( RRfld freeLMod I ) ) |-> ( sqrt ` ( x ( .i ` ( RRfld freeLMod I ) ) x ) ) ) ) ) )
17 13 14 16 sylancl 
 |-  ( I e. V -> ( dim ` ( RRfld freeLMod I ) ) = ( dim ` ( ( RRfld freeLMod I ) toNrmGrp ( x e. ( Base ` ( RRfld freeLMod I ) ) |-> ( sqrt ` ( x ( .i ` ( RRfld freeLMod I ) ) x ) ) ) ) ) )
18 11 frlmdim 
 |-  ( ( RRfld e. DivRing /\ I e. V ) -> ( dim ` ( RRfld freeLMod I ) ) = ( # ` I ) )
19 10 18 mpan 
 |-  ( I e. V -> ( dim ` ( RRfld freeLMod I ) ) = ( # ` I ) )
20 8 17 19 3eqtr2d 
 |-  ( I e. V -> ( dim ` H ) = ( # ` I ) )