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 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
Assertion tngdim ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) → ( dim ‘ 𝐺 ) = ( dim ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 tnglvec.t 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 eqidd ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
3 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4 1 3 tngbas ( 𝑁𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑇 ) )
5 4 adantl ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑇 ) )
6 ssidd ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) → ( Base ‘ 𝐺 ) ⊆ ( Base ‘ 𝐺 ) )
7 eqid ( +g𝐺 ) = ( +g𝐺 )
8 1 7 tngplusg ( 𝑁𝑉 → ( +g𝐺 ) = ( +g𝑇 ) )
9 8 adantl ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) → ( +g𝐺 ) = ( +g𝑇 ) )
10 9 oveqdr ( ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g𝐺 ) 𝑦 ) = ( 𝑥 ( +g𝑇 ) 𝑦 ) )
11 lveclmod ( 𝐺 ∈ LVec → 𝐺 ∈ LMod )
12 eqid ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝐺 )
13 eqid ( ·𝑠𝐺 ) = ( ·𝑠𝐺 )
14 eqid ( Base ‘ ( Scalar ‘ 𝐺 ) ) = ( Base ‘ ( Scalar ‘ 𝐺 ) )
15 3 12 13 14 lmodvscl ( ( 𝐺 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑥 ( ·𝑠𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
16 15 3expb ( ( 𝐺 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( ·𝑠𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
17 11 16 sylan ( ( 𝐺 ∈ LVec ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( ·𝑠𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
18 17 adantlr ( ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( ·𝑠𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
19 1 13 tngvsca ( 𝑁𝑉 → ( ·𝑠𝐺 ) = ( ·𝑠𝑇 ) )
20 19 adantl ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) → ( ·𝑠𝐺 ) = ( ·𝑠𝑇 ) )
21 20 oveqdr ( ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( ·𝑠𝐺 ) 𝑦 ) = ( 𝑥 ( ·𝑠𝑇 ) 𝑦 ) )
22 eqid ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
23 eqidd ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) → ( Base ‘ ( Scalar ‘ 𝐺 ) ) = ( Base ‘ ( Scalar ‘ 𝐺 ) ) )
24 1 12 tngsca ( 𝑁𝑉 → ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝑇 ) )
25 24 adantl ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) → ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝑇 ) )
26 25 fveq2d ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) → ( Base ‘ ( Scalar ‘ 𝐺 ) ) = ( Base ‘ ( Scalar ‘ 𝑇 ) ) )
27 25 fveq2d ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) → ( +g ‘ ( Scalar ‘ 𝐺 ) ) = ( +g ‘ ( Scalar ‘ 𝑇 ) ) )
28 27 oveqdr ( ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ) ) → ( 𝑥 ( +g ‘ ( Scalar ‘ 𝐺 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ ( Scalar ‘ 𝑇 ) ) 𝑦 ) )
29 simpl ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) → 𝐺 ∈ LVec )
30 1 tnglvec ( 𝑁𝑉 → ( 𝐺 ∈ LVec ↔ 𝑇 ∈ LVec ) )
31 30 biimpac ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) → 𝑇 ∈ LVec )
32 2 5 6 10 18 21 12 22 23 26 28 29 31 dimpropd ( ( 𝐺 ∈ LVec ∧ 𝑁𝑉 ) → ( dim ‘ 𝐺 ) = ( dim ‘ 𝑇 ) )