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

Definition df-tcph 23884
 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-tcph toℂPreHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))))
Distinct variable group:   𝑥,𝑤

Detailed syntax breakdown of Definition df-tcph
StepHypRef Expression
1 ctcph 23882 . 2 class toℂPreHil
2 vw . . 3 setvar 𝑤
3 cvv 3409 . . 3 class V
42cv 1537 . . . 4 class 𝑤
5 vx . . . . 5 setvar 𝑥
6 cbs 16555 . . . . . 6 class Base
74, 6cfv 6340 . . . . 5 class (Base‘𝑤)
85cv 1537 . . . . . . 7 class 𝑥
9 cip 16642 . . . . . . . 8 class ·𝑖
104, 9cfv 6340 . . . . . . 7 class (·𝑖𝑤)
118, 8, 10co 7156 . . . . . 6 class (𝑥(·𝑖𝑤)𝑥)
12 csqrt 14653 . . . . . 6 class
1311, 12cfv 6340 . . . . 5 class (√‘(𝑥(·𝑖𝑤)𝑥))
145, 7, 13cmpt 5116 . . . 4 class (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))
15 ctng 23294 . . . 4 class toNrmGrp
164, 14, 15co 7156 . . 3 class (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥))))
172, 3, 16cmpt 5116 . 2 class (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))))
181, 17wceq 1538 1 wff toℂPreHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖𝑤)𝑥)))))
 Colors of variables: wff setvar class This definition is referenced by:  tcphval  23932
 Copyright terms: Public domain W3C validator