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

Definition df-tch 22134
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  |- toCHil  =  ( w  e.  _V  |->  ( w toNrmGrp  ( x  e.  ( Base `  w
)  |->  ( sqr `  (
x ( .i `  w ) x ) ) ) ) )
Distinct variable group:    x, w

Detailed syntax breakdown of Definition df-tch
StepHypRef Expression
1 ctch 22132 . 2  class toCHil
2 vw . . 3  setvar  w
3 cvv 3081 . . 3  class  _V
42cv 1436 . . . 4  class  w
5 vx . . . . 5  setvar  x
6 cbs 15109 . . . . . 6  class  Base
74, 6cfv 5598 . . . . 5  class  ( Base `  w )
85cv 1436 . . . . . . 7  class  x
9 cip 15183 . . . . . . . 8  class  .i
104, 9cfv 5598 . . . . . . 7  class  ( .i
`  w )
118, 8, 10co 6302 . . . . . 6  class  ( x ( .i `  w
) x )
12 csqrt 13285 . . . . . 6  class  sqr
1311, 12cfv 5598 . . . . 5  class  ( sqr `  ( x ( .i
`  w ) x ) )
145, 7, 13cmpt 4479 . . . 4  class  ( x  e.  ( Base `  w
)  |->  ( sqr `  (
x ( .i `  w ) x ) ) )
15 ctng 21580 . . . 4  class toNrmGrp
164, 14, 15co 6302 . . 3  class  ( w toNrmGrp  ( x  e.  ( Base `  w )  |->  ( sqr `  ( x ( .i `  w
) x ) ) ) )
172, 3, 16cmpt 4479 . 2  class  ( w  e.  _V  |->  ( w toNrmGrp  ( x  e.  ( Base `  w )  |->  ( sqr `  ( x ( .i `  w
) x ) ) ) ) )
181, 17wceq 1437 1  wff toCHil  =  ( w  e.  _V  |->  ( w toNrmGrp  ( x  e.  ( Base `  w
)  |->  ( sqr `  (
x ( .i `  w ) x ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  tchval  22179
  Copyright terms: Public domain W3C validator