Metamath Proof Explorer


Theorem nmf

Description: The norm on a normed group is a function into the reals. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses nmf.x 𝑋 = ( Base ‘ 𝐺 )
nmf.n 𝑁 = ( norm ‘ 𝐺 )
Assertion nmf ( 𝐺 ∈ NrmGrp → 𝑁 : 𝑋 ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 nmf.x 𝑋 = ( Base ‘ 𝐺 )
2 nmf.n 𝑁 = ( norm ‘ 𝐺 )
3 ngpgrp ( 𝐺 ∈ NrmGrp → 𝐺 ∈ Grp )
4 eqid ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) ) = ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) )
5 1 4 ngpmet ( 𝐺 ∈ NrmGrp → ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) )
6 eqid ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
7 2 1 6 4 nmf2 ( ( 𝐺 ∈ Grp ∧ ( ( dist ‘ 𝐺 ) ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) ) → 𝑁 : 𝑋 ⟶ ℝ )
8 3 5 7 syl2anc ( 𝐺 ∈ NrmGrp → 𝑁 : 𝑋 ⟶ ℝ )