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\mathrm{toNrmGrp}N$$
Assertion	tnglvec	$$⊢N\in V\to \left(G\in \mathrm{LVec}\leftrightarrow T\in \mathrm{LVec}\right)$$

Proof

Step	Hyp	Ref	Expression
1		tnglvec.t	$$⊢T=G\mathrm{toNrmGrp}N$$
2		eqidd	$$⊢N\in V\to {\mathrm{Base}}_G={\mathrm{Base}}_G$$
3		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
4	1 3	tngbas	$$⊢N\in V\to {\mathrm{Base}}_G={\mathrm{Base}}_T$$
5		eqid	$$⊢{+}_G={+}_G$$
6	1 5	tngplusg	$$⊢N\in V\to {+}_G={+}_T$$
7	6	oveqdr	$$⊢\left(N\in V\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to x{+}_{G}y=x{+}_{T}y$$
8		eqidd	$$⊢N\in V\to \mathrm{Scalar}\left(G\right)=\mathrm{Scalar}\left(G\right)$$
9		eqid	$$⊢\mathrm{Scalar}\left(G\right)=\mathrm{Scalar}\left(G\right)$$
10	1 9	tngsca	$$⊢N\in V\to \mathrm{Scalar}\left(G\right)=\mathrm{Scalar}\left(T\right)$$
11		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(G\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(G\right)}$$
12		eqid	$$⊢{\cdot }_G={\cdot }_G$$
13	1 12	tngvsca	$$⊢N\in V\to {\cdot }_G={\cdot }_T$$
14	13	oveqdr	$$⊢\left(N\in V\wedge \left(x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(G\right)}\wedge y\in {\mathrm{Base}}_G\right)\right)\to x{\cdot }_{G}y=x{\cdot }_{T}y$$
15	2 4 7 8 10 11 14	lvecpropd	$$⊢N\in V\to \left(G\in \mathrm{LVec}\leftrightarrow T\in \mathrm{LVec}\right)$$