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