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 \in V \land T \in NrmGrp) \to G \in Grp$

Step	Hyp	Ref	Expression
1		tngngp3.t	$⊢ T = G toNrmGrp N$
2		eqid	$⊢ {Base}_{G} = {Base}_{G}$
3	1 2	tngbas	$⊢ N \in V \to {Base}_{G} = {Base}_{T}$
4		eqidd	$⊢ N \in V \to {Base}_{G} = {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	$⊢ (N \in V \land (x \in {Base}_{G} \land y \in {Base}_{G})) \to x +_{T} y = x +_{G} y$
9	3 4 8	grppropd	$⊢ N \in V \to (T \in Grp \leftrightarrow G \in Grp)$
10	9	biimpd	$⊢ N \in V \to (T \in Grp \to G \in Grp)$
11		ngpgrp	$⊢ T \in NrmGrp \to T \in Grp$
12	10 11	impel	$⊢ (N \in V \land T \in NrmGrp) \to G \in Grp$

Metamath Proof Explorer