Theorem 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	⊢ 𝑇 = ( 𝐺 toNrmGrp ( norm ‘ 𝐺 ) )
Assertion	nrmtngnrm	⊢ ( 𝐺 ∈ NrmGrp → ( 𝑇 ∈ NrmGrp ∧ ( norm ‘ 𝑇 ) = ( norm ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nrmtngdist.t	⊢ 𝑇 = ( 𝐺 toNrmGrp ( norm ‘ 𝐺 ) )
2		ngpgrp	⊢ ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
3		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4	1 3	nrmtngdist	⊢ ( 𝐺 ∈ NrmGrp → ( dist ‘ 𝑇 ) = ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) )
5		eqid	⊢ ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) = ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) )
6	3 5	ngpmet	⊢ ( 𝐺 ∈ NrmGrp → ( ( dist ‘ 𝐺 ) ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝐺 ) ) )
7	4 6	eqeltrd	⊢ ( 𝐺 ∈ NrmGrp → ( dist ‘ 𝑇 ) ∈ ( Met ‘ ( Base ‘ 𝐺 ) ) )
8		eqid	⊢ ( norm ‘ 𝐺 ) = ( norm ‘ 𝐺 )
9	3 8	nmf	⊢ ( 𝐺 ∈ NrmGrp → ( norm ‘ 𝐺 ) : ( Base ‘ 𝐺 ) ⟶ ℝ )
10		eqid	⊢ ( dist ‘ 𝑇 ) = ( dist ‘ 𝑇 )
11	1 3 10	tngngp2	⊢ ( ( norm ‘ 𝐺 ) : ( Base ‘ 𝐺 ) ⟶ ℝ → ( 𝑇 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ ( dist ‘ 𝑇 ) ∈ ( Met ‘ ( Base ‘ 𝐺 ) ) ) ) )
12	9 11	syl	⊢ ( 𝐺 ∈ NrmGrp → ( 𝑇 ∈ NrmGrp ↔ ( 𝐺 ∈ Grp ∧ ( dist ‘ 𝑇 ) ∈ ( Met ‘ ( Base ‘ 𝐺 ) ) ) ) )
13	2 7 12	mpbir2and	⊢ ( 𝐺 ∈ NrmGrp → 𝑇 ∈ NrmGrp )
14	2 9	jca	⊢ ( 𝐺 ∈ NrmGrp → ( 𝐺 ∈ Grp ∧ ( norm ‘ 𝐺 ) : ( Base ‘ 𝐺 ) ⟶ ℝ ) )
15		reex	⊢ ℝ ∈ V
16	1 3 15	tngnm	⊢ ( ( 𝐺 ∈ Grp ∧ ( norm ‘ 𝐺 ) : ( Base ‘ 𝐺 ) ⟶ ℝ ) → ( norm ‘ 𝐺 ) = ( norm ‘ 𝑇 ) )
17	14 16	syl	⊢ ( 𝐺 ∈ NrmGrp → ( norm ‘ 𝐺 ) = ( norm ‘ 𝑇 ) )
18	17	eqcomd	⊢ ( 𝐺 ∈ NrmGrp → ( norm ‘ 𝑇 ) = ( norm ‘ 𝐺 ) )
19	13 18	jca	⊢ ( 𝐺 ∈ NrmGrp → ( 𝑇 ∈ NrmGrp ∧ ( norm ‘ 𝑇 ) = ( norm ‘ 𝐺 ) ) )