Database
BASIC TOPOLOGY
Metric spaces
Normed algebraic structures
nmfval2
Metamath Proof Explorer
Description: The value of the norm function on a group as the distance restricted to
the elements of the base set to zero. (Contributed by Mario Carneiro , 2-Oct-2015)
Ref
Expression
Hypotheses
nmfval2.n
⊢ 𝑁 = ( norm ‘ 𝑊 )
nmfval2.x
⊢ 𝑋 = ( Base ‘ 𝑊 )
nmfval2.z
⊢ 0 = ( 0g ‘ 𝑊 )
nmfval2.d
⊢ 𝐷 = ( dist ‘ 𝑊 )
nmfval2.e
⊢ 𝐸 = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) )
Assertion
nmfval2
⊢ ( 𝑊 ∈ Grp → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐸 0 ) ) )
Proof
Step
Hyp
Ref
Expression
1
nmfval2.n
⊢ 𝑁 = ( norm ‘ 𝑊 )
2
nmfval2.x
⊢ 𝑋 = ( Base ‘ 𝑊 )
3
nmfval2.z
⊢ 0 = ( 0g ‘ 𝑊 )
4
nmfval2.d
⊢ 𝐷 = ( dist ‘ 𝑊 )
5
nmfval2.e
⊢ 𝐸 = ( 𝐷 ↾ ( 𝑋 × 𝑋 ) )
6
2 3
grpidcl
⊢ ( 𝑊 ∈ Grp → 0 ∈ 𝑋 )
7
1 2 3 4 5
nmfval0
⊢ ( 0 ∈ 𝑋 → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐸 0 ) ) )
8
6 7
syl
⊢ ( 𝑊 ∈ Grp → 𝑁 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 𝐸 0 ) ) )