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 ⊢ T = G toNrmGrp N
Assertion tnglvec ⊢ N ∈ V → G ∈ LVec ↔ T ∈ LVec

Proof

Step Hyp Ref Expression
1 tnglvec.t ⊢ T = G toNrmGrp N
2 eqidd ⊢ N ∈ V → Base G = Base G
3 eqid ⊢ Base G = Base G
4 1 3 tngbas ⊢ N ∈ V → Base G = Base T
5 eqid ⊢ + G = + G
6 1 5 tngplusg ⊢ N ∈ V → + G = + T
7 6 oveqdr ⊢ N ∈ V ∧ x ∈ Base G ∧ y ∈ Base G → x + G y = x + T y
8 eqidd ⊢ N ∈ V → Scalar ⁡ G = Scalar ⁡ G
9 eqid ⊢ Scalar ⁡ G = Scalar ⁡ G
10 1 9 tngsca ⊢ N ∈ V → Scalar ⁡ G = Scalar ⁡ T
11 eqid ⊢ Base Scalar ⁡ G = Base Scalar ⁡ G
12 eqid ⊢ ⋅ G = ⋅ G
13 1 12 tngvsca ⊢ N ∈ V → ⋅ G = ⋅ T
14 13 oveqdr ⊢ N ∈ V ∧ x ∈ Base Scalar ⁡ G ∧ y ∈ Base G → x ⋅ G y = x ⋅ T y
15 2 4 7 8 10 11 14 lvecpropd ⊢ N ∈ V → G ∈ LVec ↔ T ∈ LVec