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 → 𝑁 : 𝑋 ⟶ ℝ ) |
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 → 𝑁 : 𝑋 ⟶ ℝ ) |