Theorem tnggrpr

Description: If a structure equipped with a norm is a normed group, the structure itself must be a group. (Contributed by AV, 15-Oct-2021)

	Ref	Expression
Hypothesis	tngngp3.t	$$⊢T=G\mathrm{toNrmGrp}N$$
Assertion	tnggrpr	$$⊢\left(N\in V\wedge T\in \mathrm{NrmGrp}\right)\to G\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		tngngp3.t	$$⊢T=G\mathrm{toNrmGrp}N$$
2		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
3	1 2	tngbas	$$⊢N\in V\to {\mathrm{Base}}_G={\mathrm{Base}}_T$$
4		eqidd	$$⊢N\in V\to {\mathrm{Base}}_G={\mathrm{Base}}_G$$
5		eqid	$$⊢{+}_G={+}_G$$
6	1 5	tngplusg	$$⊢N\in V\to {+}_G={+}_T$$
7	6	eqcomd	$$⊢N\in V\to {+}_T={+}_G$$
8	7	oveqdr	$$⊢\left(N\in V\wedge \left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\right)\to x{+}_{T}y=x{+}_{G}y$$
9	3 4 8	grppropd	$$⊢N\in V\to \left(T\in \mathrm{Grp}\leftrightarrow G\in \mathrm{Grp}\right)$$
10	9	biimpd	$$⊢N\in V\to \left(T\in \mathrm{Grp}\to G\in \mathrm{Grp}\right)$$
11		ngpgrp	$$⊢T\in \mathrm{NrmGrp}\to T\in \mathrm{Grp}$$
12	10 11	impel	$$⊢\left(N\in V\wedge T\in \mathrm{NrmGrp}\right)\to G\in \mathrm{Grp}$$