This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑇 = ( 𝐺 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 ‘ 𝐺 ) ) )