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

Definition df-tch 22950
 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 subcomplex 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 22948 . 2 class toℂHil
2 vw . . 3 setvar 𝑤
3 cvv 3195 . . 3 class V
42cv 1480 . . . 4 class 𝑤
5 vx . . . . 5 setvar 𝑥
6 cbs 15838 . . . . . 6 class Base
74, 6cfv 5876 . . . . 5 class (Base‘𝑤)
85cv 1480 . . . . . . 7 class 𝑥
9 cip 15927 . . . . . . . 8 class ·𝑖
104, 9cfv 5876 . . . . . . 7 class (·𝑖𝑤)
118, 8, 10co 6635 . . . . . 6 class (𝑥(·𝑖𝑤)𝑥)
12 csqrt 13954 . . . . . 6 class
1311, 12cfv 5876 . . . . 5 class (√‘(𝑥(·𝑖𝑤)𝑥))
145, 7, 13cmpt 4720 . . . 4 class (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))
15 ctng 22364 . . . 4 class toNrmGrp
164, 14, 15co 6635 . . 3 class (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
172, 3, 16cmpt 4720 . 2 class (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))))
181, 17wceq 1481 1 wff toℂHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))))
 Colors of variables: wff setvar class This definition is referenced by:  tchval  22998
 Copyright terms: Public domain W3C validator