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

Metamath Proof Explorer

Theorem tcphds

Description: The distance of a pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Hypotheses tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
tcphds.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
tcphds.m ⊢ − = ( -g ‘ 𝑊 )
Assertion tcphds ( 𝑊 ∈ Grp → ( 𝑁 ∘ − ) = ( dist ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
2 tcphds.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
3 tcphds.m ⊢ − = ( -g ‘ 𝑊 )
4 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
5 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
6 1 2 4 5 tchnmfval ⊢ ( 𝑊 ∈ Grp → 𝑁 = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) )
7 6 coeq1d ⊢ ( 𝑊 ∈ Grp → ( 𝑁 ∘ − ) = ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) ∘ − ) )
8 4 tcphex ⊢ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) ∈ V
9 1 4 5 tcphval ⊢ 𝐺 = ( 𝑊 toNrmGrp ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) )
10 9 3 tngds ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) ∈ V → ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) ∘ − ) = ( dist ‘ 𝐺 ) )
11 8 10 ax-mp ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) ∘ − ) = ( dist ‘ 𝐺 )
12 7 11 eqtrdi ⊢ ( 𝑊 ∈ Grp → ( 𝑁 ∘ − ) = ( dist ‘ 𝐺 ) )