nrmtngnrm

Description: The augmentation of a normed group by its own norm is a normed group with the same norm. (Contributed by AV, 15-Oct-2021)

		Ref	Expression
	Hypothesis	nrmtngdist.t	$⊢ T = G toNrmGrp norm (G)$
	Assertion	nrmtngnrm	$⊢ G \in NrmGrp \to (T \in NrmGrp \land norm (T) = norm (G))$

Step	Hyp	Ref	Expression
1		nrmtngdist.t	$⊢ T = G toNrmGrp norm (G)$
2		ngpgrp	$⊢ G \in NrmGrp \to G \in Grp$
3		eqid	$⊢ {Base}_{G} = {Base}_{G}$
4	1 3	nrmtngdist	$⊢ G \in NrmGrp \to dist (T) = {dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}$
5		eqid	$⊢ {dist (G) ↾}_{({Base}_{G} \times {Base}_{G})} = {dist (G) ↾}_{({Base}_{G} \times {Base}_{G})}$
6	3 5	ngpmet	$⊢ G \in NrmGrp \to {dist (G) ↾}_{({Base}_{G} \times {Base}_{G})} \in Met ({Base}_{G})$
7	4 6	eqeltrd	$⊢ G \in NrmGrp \to dist (T) \in Met ({Base}_{G})$
8		eqid	$⊢ norm (G) = norm (G)$
9	3 8	nmf	$⊢ G \in NrmGrp \to norm (G) : {Base}_{G} ⟶ ℝ$
10		eqid	$⊢ dist (T) = dist (T)$
11	1 3 10	tngngp2	$⊢ norm (G) : {Base}_{G} ⟶ ℝ \to (T \in NrmGrp \leftrightarrow (G \in Grp \land dist (T) \in Met ({Base}_{G})))$
12	9 11	syl	$⊢ G \in NrmGrp \to (T \in NrmGrp \leftrightarrow (G \in Grp \land dist (T) \in Met ({Base}_{G})))$
13	2 7 12	mpbir2and	$⊢ G \in NrmGrp \to T \in NrmGrp$
14	2 9	jca	$⊢ G \in NrmGrp \to (G \in Grp \land norm (G) : {Base}_{G} ⟶ ℝ)$
15		reex	$⊢ ℝ \in V$
16	1 3 15	tngnm	$⊢ (G \in Grp \land norm (G) : {Base}_{G} ⟶ ℝ) \to norm (G) = norm (T)$
17	14 16	syl	$⊢ G \in NrmGrp \to norm (G) = norm (T)$
18	17	eqcomd	$⊢ G \in NrmGrp \to norm (T) = norm (G)$
19	13 18	jca	$⊢ G \in NrmGrp \to (T \in NrmGrp \land norm (T) = norm (G))$

Metamath Proof Explorer