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=GtoNrmGrpN
Assertion tngdim ⊢G∈LVec∧N∈V→dim⁡G=dim⁡T

Proof

Step Hyp Ref Expression
1 tnglvec.t ⊢T=GtoNrmGrpN
2 eqidd ⊢G∈LVec∧N∈V→BaseG=BaseG
3 eqid ⊢BaseG=BaseG
4 1 3 tngbas ⊢N∈V→BaseG=BaseT
5 4 adantl ⊢G∈LVec∧N∈V→BaseG=BaseT
6 ssidd ⊢G∈LVec∧N∈V→BaseG⊆BaseG
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∈BaseG∧y∈BaseG→x+Gy=x+Ty
11 lveclmod ⊢G∈LVec→G∈LMod
12 eqid ⊢Scalar⁡G=Scalar⁡G
13 eqid ⊢⋅G=⋅G
14 eqid ⊢BaseScalar⁡G=BaseScalar⁡G
15 3 12 13 14 lmodvscl ⊢G∈LMod∧x∈BaseScalar⁡G∧y∈BaseG→x⋅Gy∈BaseG
16 15 3expb ⊢G∈LMod∧x∈BaseScalar⁡G∧y∈BaseG→x⋅Gy∈BaseG
17 11 16 sylan ⊢G∈LVec∧x∈BaseScalar⁡G∧y∈BaseG→x⋅Gy∈BaseG
18 17 adantlr ⊢G∈LVec∧N∈V∧x∈BaseScalar⁡G∧y∈BaseG→x⋅Gy∈BaseG
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∈BaseScalar⁡G∧y∈BaseG→x⋅Gy=x⋅Ty
22 eqid ⊢Scalar⁡T=Scalar⁡T
23 eqidd ⊢G∈LVec∧N∈V→BaseScalar⁡G=BaseScalar⁡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→BaseScalar⁡G=BaseScalar⁡T
27 25 fveq2d ⊢G∈LVec∧N∈V→+Scalar⁡G=+Scalar⁡T
28 27 oveqdr ⊢G∈LVec∧N∈V∧x∈BaseScalar⁡G∧y∈BaseScalar⁡G→x+Scalar⁡Gy=x+Scalar⁡Ty
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