Metamath Proof Explorer

Theorem tngdim

Description: Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023)

Ref Expression
Hypothesis tnglvec.t 
|- T = ( G toNrmGrp N )
Assertion tngdim 
|- ( ( G e. LVec /\ N e. V ) -> ( dim ` G ) = ( dim ` T ) )

Proof

Step Hyp Ref Expression
1 tnglvec.t 
 |-  T = ( G toNrmGrp N )
2 eqidd 
 |-  ( ( G e. LVec /\ N e. V ) -> ( Base ` G ) = ( Base ` G ) )
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 1 3 tngbas 
 |-  ( N e. V -> ( Base ` G ) = ( Base ` T ) )
5 4 adantl 
 |-  ( ( G e. LVec /\ N e. V ) -> ( Base ` G ) = ( Base ` T ) )
6 ssidd 
 |-  ( ( G e. LVec /\ N e. V ) -> ( Base ` G ) C_ ( Base ` G ) )
7 eqid 
 |-  ( +g ` G ) = ( +g ` G )
8 1 7 tngplusg 
 |-  ( N e. V -> ( +g ` G ) = ( +g ` T ) )
9 8 adantl 
 |-  ( ( G e. LVec /\ N e. V ) -> ( +g ` G ) = ( +g ` T ) )
10 9 oveqdr 
 |-  ( ( ( G e. LVec /\ N e. V ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` T ) y ) )
11 lveclmod 
 |-  ( G e. LVec -> G e. LMod )
12 eqid 
 |-  ( Scalar ` G ) = ( Scalar ` G )
13 eqid 
 |-  ( .s ` G ) = ( .s ` G )
14 eqid 
 |-  ( Base ` ( Scalar ` G ) ) = ( Base ` ( Scalar ` G ) )
15 3 12 13 14 lmodvscl 
 |-  ( ( G e. LMod /\ x e. ( Base ` ( Scalar ` G ) ) /\ y e. ( Base ` G ) ) -> ( x ( .s ` G ) y ) e. ( Base ` G ) )
16 15 3expb 
 |-  ( ( G e. LMod /\ ( x e. ( Base ` ( Scalar ` G ) ) /\ y e. ( Base ` G ) ) ) -> ( x ( .s ` G ) y ) e. ( Base ` G ) )
17 11 16 sylan 
 |-  ( ( G e. LVec /\ ( x e. ( Base ` ( Scalar ` G ) ) /\ y e. ( Base ` G ) ) ) -> ( x ( .s ` G ) y ) e. ( Base ` G ) )
18 17 adantlr 
 |-  ( ( ( G e. LVec /\ N e. V ) /\ ( x e. ( Base ` ( Scalar ` G ) ) /\ y e. ( Base ` G ) ) ) -> ( x ( .s ` G ) y ) e. ( Base ` G ) )
19 1 13 tngvsca 
 |-  ( N e. V -> ( .s ` G ) = ( .s ` T ) )
20 19 adantl 
 |-  ( ( G e. LVec /\ N e. V ) -> ( .s ` G ) = ( .s ` T ) )
21 20 oveqdr 
 |-  ( ( ( G e. LVec /\ N e. V ) /\ ( x e. ( Base ` ( Scalar ` G ) ) /\ y e. ( Base ` G ) ) ) -> ( x ( .s ` G ) y ) = ( x ( .s ` T ) y ) )
22 eqid 
 |-  ( Scalar ` T ) = ( Scalar ` T )
23 eqidd 
 |-  ( ( G e. LVec /\ N e. V ) -> ( Base ` ( Scalar ` G ) ) = ( Base ` ( Scalar ` G ) ) )
24 1 12 tngsca 
 |-  ( N e. V -> ( Scalar ` G ) = ( Scalar ` T ) )
25 24 adantl 
 |-  ( ( G e. LVec /\ N e. V ) -> ( Scalar ` G ) = ( Scalar ` T ) )
26 25 fveq2d 
 |-  ( ( G e. LVec /\ N e. V ) -> ( Base ` ( Scalar ` G ) ) = ( Base ` ( Scalar ` T ) ) )
27 25 fveq2d 
 |-  ( ( G e. LVec /\ N e. V ) -> ( +g ` ( Scalar ` G ) ) = ( +g ` ( Scalar ` T ) ) )
28 27 oveqdr 
 |-  ( ( ( G e. LVec /\ N e. V ) /\ ( x e. ( Base ` ( Scalar ` G ) ) /\ y e. ( Base ` ( Scalar ` G ) ) ) ) -> ( x ( +g ` ( Scalar ` G ) ) y ) = ( x ( +g ` ( Scalar ` T ) ) y ) )
29 simpl 
 |-  ( ( G e. LVec /\ N e. V ) -> G e. LVec )
30 1 tnglvec 
 |-  ( N e. V -> ( G e. LVec <-> T e. LVec ) )
31 30 biimpac 
 |-  ( ( G e. LVec /\ N e. V ) -> T e. LVec )
32 2 5 6 10 18 21 12 22 23 26 28 29 31 dimpropd 
 |-  ( ( G e. LVec /\ N e. V ) -> ( dim ` G ) = ( dim ` T ) )