MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tch Structured version   Visualization version   GIF version

Definition df-tch 22697
Description: Define a function to augment a (pre-)Hilbert space with a norm. No extra parameters are needed, but some conditions must be satisfied to ensure that this in fact creates a normed pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.)
Assertion
Ref Expression
df-tch toℂHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))))
Distinct variable group:   𝑥,𝑤

Detailed syntax breakdown of Definition df-tch
StepHypRef Expression
1 ctch 22695 . 2 class toℂHil
2 vw . . 3 setvar 𝑤
3 cvv 3168 . . 3 class V
42cv 1473 . . . 4 class 𝑤
5 vx . . . . 5 setvar 𝑥
6 cbs 15637 . . . . . 6 class Base
74, 6cfv 5786 . . . . 5 class (Base‘𝑤)
85cv 1473 . . . . . . 7 class 𝑥
9 cip 15715 . . . . . . . 8 class ·𝑖
104, 9cfv 5786 . . . . . . 7 class (·𝑖𝑤)
118, 8, 10co 6523 . . . . . 6 class (𝑥(·𝑖𝑤)𝑥)
12 csqrt 13763 . . . . . 6 class
1311, 12cfv 5786 . . . . 5 class (√‘(𝑥(·𝑖𝑤)𝑥))
145, 7, 13cmpt 4633 . . . 4 class (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))
15 ctng 22130 . . . 4 class toNrmGrp
164, 14, 15co 6523 . . 3 class (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
172, 3, 16cmpt 4633 . 2 class (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))))
181, 17wceq 1474 1 wff toℂHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))))
Colors of variables: wff setvar class
This definition is referenced by:  tchval  22742
  Copyright terms: Public domain W3C validator