Metamath Proof Explorer

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 ⊢ T = G toNrmGrp norm ⁡ G
Assertion nrmtngnrm ⊢ G ∈ NrmGrp → T ∈ NrmGrp ∧ norm ⁡ T = norm ⁡ G

Proof

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