Metamath Proof Explorer

Theorem nmf2

Description: The norm on a metric group is a function from the base set into the reals. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses nmf2.n ⊢ N = norm ⁡ W
nmf2.x ⊢ X = Base W
nmf2.d ⊢ D = dist ⁡ W
nmf2.e ⊢ E = D ↾ X × X
Assertion nmf2 ⊢ W ∈ Grp ∧ E ∈ Met ⁡ X → N : X ⟶ ℝ

Proof

Step Hyp Ref Expression
1 nmf2.n ⊢ N = norm ⁡ W
2 nmf2.x ⊢ X = Base W
3 nmf2.d ⊢ D = dist ⁡ W
4 nmf2.e ⊢ E = D ↾ X × X
5 eqid ⊢ 0 W = 0 W
6 1 2 5 3 4 nmfval2 ⊢ W ∈ Grp → N = x ∈ X ⟼ x E 0 W
7 6 adantr ⊢ W ∈ Grp ∧ E ∈ Met ⁡ X → N = x ∈ X ⟼ x E 0 W
8 2 5 grpidcl ⊢ W ∈ Grp → 0 W ∈ X
9 metcl ⊢ E ∈ Met ⁡ X ∧ x ∈ X ∧ 0 W ∈ X → x E 0 W ∈ ℝ
10 9 3comr ⊢ 0 W ∈ X ∧ E ∈ Met ⁡ X ∧ x ∈ X → x E 0 W ∈ ℝ
11 8 10 syl3an1 ⊢ W ∈ Grp ∧ E ∈ Met ⁡ X ∧ x ∈ X → x E 0 W ∈ ℝ
12 11 3expa ⊢ W ∈ Grp ∧ E ∈ Met ⁡ X ∧ x ∈ X → x E 0 W ∈ ℝ
13 7 12 fmpt3d ⊢ W ∈ Grp ∧ E ∈ Met ⁡ X → N : X ⟶ ℝ