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 LVec N V dim G = dim T

Proof

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