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

Definition df-tch 22777
 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 22775 . 2 class toℂHil
2 vw . . 3 setvar 𝑤
3 cvv 3173 . . 3 class V
42cv 1474 . . . 4 class 𝑤
5 vx . . . . 5 setvar 𝑥
6 cbs 15695 . . . . . 6 class Base
74, 6cfv 5804 . . . . 5 class (Base‘𝑤)
85cv 1474 . . . . . . 7 class 𝑥
9 cip 15773 . . . . . . . 8 class ·𝑖
104, 9cfv 5804 . . . . . . 7 class (·𝑖𝑤)
118, 8, 10co 6549 . . . . . 6 class (𝑥(·𝑖𝑤)𝑥)
12 csqrt 13821 . . . . . 6 class
1311, 12cfv 5804 . . . . 5 class (√‘(𝑥(·𝑖𝑤)𝑥))
145, 7, 13cmpt 4643 . . . 4 class (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))
15 ctng 22193 . . . 4 class toNrmGrp
164, 14, 15co 6549 . . 3 class (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
172, 3, 16cmpt 4643 . 2 class (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))))
181, 17wceq 1475 1 wff toℂHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))))
 Colors of variables: wff setvar class This definition is referenced by:  tchval  22825
 Copyright terms: Public domain W3C validator