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

Metamath Proof Explorer

Theorem 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 ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
Assertion tnggrpr ( ( 𝑁 ∈ 𝑉 ∧ 𝑇 ∈ NrmGrp ) → 𝐺 ∈ Grp )

Proof

Step Hyp Ref Expression
1 tngngp3.t ⊢ 𝑇 = ( 𝐺 toNrmGrp 𝑁 )
2 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3 1 2 tngbas ⊢ ( 𝑁 ∈ 𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑇 ) )
4 eqidd ⊢ ( 𝑁 ∈ 𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
5 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
6 1 5 tngplusg ⊢ ( 𝑁 ∈ 𝑉 → ( +g ‘ 𝐺 ) = ( +g ‘ 𝑇 ) )
7 6 eqcomd ⊢ ( 𝑁 ∈ 𝑉 → ( +g ‘ 𝑇 ) = ( +g ‘ 𝐺 ) )
8 7 oveqdr ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ( 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ) → ( 𝑥 ( +g ‘ 𝑇 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
9 3 4 8 grppropd ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑇 ∈ Grp ↔ 𝐺 ∈ Grp ) )
10 9 biimpd ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑇 ∈ Grp → 𝐺 ∈ Grp ) )
11 ngpgrp ⊢ ( 𝑇 ∈ NrmGrp → 𝑇 ∈ Grp )
12 10 11 impel ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑇 ∈ NrmGrp ) → 𝐺 ∈ Grp )