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 ⊢ G = toCPreHil ⁡ W
tcphds.n ⊢ N = norm ⁡ G
tcphds.m ⊢ - ˙ = - W
Assertion tcphds ⊢ W ∈ Grp → N ∘ - ˙ = dist ⁡ G

Proof

Step Hyp Ref Expression
1 tcphval.n ⊢ G = toCPreHil ⁡ W
2 tcphds.n ⊢ N = norm ⁡ G
3 tcphds.m ⊢ - ˙ = - W
4 eqid ⊢ Base W = Base W
5 eqid ⊢ ⋅ 𝑖 ⁡ W = ⋅ 𝑖 ⁡ W
6 1 2 4 5 tchnmfval ⊢ W ∈ Grp → N = x ∈ Base W ⟼ x ⋅ 𝑖 ⁡ W x
7 6 coeq1d ⊢ W ∈ Grp → N ∘ - ˙ = x ∈ Base W ⟼ x ⋅ 𝑖 ⁡ W x ∘ - ˙
8 4 tcphex ⊢ x ∈ Base W ⟼ x ⋅ 𝑖 ⁡ W x ∈ V
9 1 4 5 tcphval ⊢ G = W toNrmGrp x ∈ Base W ⟼ x ⋅ 𝑖 ⁡ W x
10 9 3 tngds ⊢ x ∈ Base W ⟼ x ⋅ 𝑖 ⁡ W x ∈ V → x ∈ Base W ⟼ x ⋅ 𝑖 ⁡ W x ∘ - ˙ = dist ⁡ G
11 8 10 ax-mp ⊢ x ∈ Base W ⟼ x ⋅ 𝑖 ⁡ W x ∘ - ˙ = dist ⁡ G
12 7 11 eqtrdi ⊢ W ∈ Grp → N ∘ - ˙ = dist ⁡ G