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 toNrmGrp N )
Assertion	tnggrpr	|- ( ( N e. V /\ T e. NrmGrp ) -> G e. Grp )

Proof

Step	Hyp	Ref	Expression
1		tngngp3.t	|- T = ( G toNrmGrp N )
2		eqid	|- ( Base ` G ) = ( Base ` G )
3	1 2	tngbas	|- ( N e. V -> ( Base ` G ) = ( Base ` T ) )
4		eqidd	|- ( N e. V -> ( Base ` G ) = ( Base ` G ) )
5		eqid	|- ( +g ` G ) = ( +g ` G )
6	1 5	tngplusg	|- ( N e. V -> ( +g ` G ) = ( +g ` T ) )
7	6	eqcomd	|- ( N e. V -> ( +g ` T ) = ( +g ` G ) )
8	7	oveqdr	|- ( ( N e. V /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( +g ` T ) y ) = ( x ( +g ` G ) y ) )
9	3 4 8	grppropd	|- ( N e. V -> ( T e. Grp <-> G e. Grp ) )
10	9	biimpd	|- ( N e. V -> ( T e. Grp -> G e. Grp ) )
11		ngpgrp	|- ( T e. NrmGrp -> T e. Grp )
12	10 11	impel	|- ( ( N e. V /\ T e. NrmGrp ) -> G e. Grp )