This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑇 ) )