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

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 ⊢ 𝑁 = ( norm ‘ 𝑊 )
nmf2.x ⊢ 𝑋 = ( Base ‘ 𝑊 )
nmf2.d ⊢ 𝐷 = ( dist ‘ 𝑊 )
nmf2.e ⊢ 𝐸 = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) )
Assertion nmf2 ( ( 𝑊 ∈ Grp ∧ 𝐸 ∈ ( Met ‘ 𝑋 ) ) → 𝑁 : 𝑋 ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 nmf2.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
2 nmf2.x ⊢ 𝑋 = ( Base ‘ 𝑊 )
3 nmf2.d ⊢ 𝐷 = ( dist ‘ 𝑊 )
4 nmf2.e ⊢ 𝐸 = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) )
5 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
6 1 2 5 3 4 nmfval2 ⊢ ( 𝑊 ∈ Grp → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐸 ( 0g ‘ 𝑊 ) ) ) )
7 6 adantr ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐸 ∈ ( Met ‘ 𝑋 ) ) → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐸 ( 0g ‘ 𝑊 ) ) ) )
8 2 5 grpidcl ⊢ ( 𝑊 ∈ Grp → ( 0g ‘ 𝑊 ) ∈ 𝑋 )
9 metcl ⊢ ( ( 𝐸 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 0g ‘ 𝑊 ) ∈ 𝑋 ) → ( 𝑥 𝐸 ( 0g ‘ 𝑊 ) ) ∈ ℝ )
10 9 3comr ⊢ ( ( ( 0g ‘ 𝑊 ) ∈ 𝑋 ∧ 𝐸 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐸 ( 0g ‘ 𝑊 ) ) ∈ ℝ )
11 8 10 syl3an1 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐸 ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐸 ( 0g ‘ 𝑊 ) ) ∈ ℝ )
12 11 3expa ⊢ ( ( ( 𝑊 ∈ Grp ∧ 𝐸 ∈ ( Met ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐸 ( 0g ‘ 𝑊 ) ) ∈ ℝ )
13 7 12 fmpt3d ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐸 ∈ ( Met ‘ 𝑋 ) ) → 𝑁 : 𝑋 ⟶ ℝ )