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

Metamath Proof Explorer

Theorem tnglvec

Description: Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023)

Ref Expression
Hypothesis tnglvec.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
Assertion tnglvec ( 𝑁 ∈ 𝑉 → ( 𝐺 ∈ LVec ↔ 𝑇 ∈ LVec ) )

Proof

Step Hyp Ref Expression
1 tnglvec.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 eqidd ⊢ ( 𝑁 ∈ 𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
3 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4 1 3 tngbas ⊢ ( 𝑁 ∈ 𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑇 ) )
5 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
6 1 5 tngplusg ⊢ ( 𝑁 ∈ 𝑉 → ( +g ‘ 𝐺 ) = ( +g ‘ 𝑇 ) )
7 6 oveqdr ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) )
8 eqidd ⊢ ( 𝑁 ∈ 𝑉 → ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝐺 ) )
9 eqid ⊢ ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝐺 )
10 1 9 tngsca ⊢ ( 𝑁 ∈ 𝑉 → ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝑇 ) )
11 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐺 ) ) = ( Base ‘ ( Scalar ‘ 𝐺 ) )
12 eqid ⊢ ( ·𝑠 ‘ 𝐺 ) = ( ·𝑠 ‘ 𝐺 )
13 1 12 tngvsca ⊢ ( 𝑁 ∈ 𝑉 → ( ·𝑠 ‘ 𝐺 ) = ( ·𝑠 ‘ 𝑇 ) )
14 13 oveqdr ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝐺 ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝑇 ) 𝑦 ) )
15 2 4 7 8 10 11 14 lvecpropd ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 ∈ LVec ↔ 𝑇 ∈ LVec ) )