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