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

Definition df-tch 21346
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 21344 . 2  class toCHil
2 vw . . 3  setvar  w
3 cvv 3108 . . 3  class  _V
42cv 1373 . . . 4  class  w
5 vx . . . . 5  setvar  x
6 cbs 14481 . . . . . 6  class  Base
74, 6cfv 5581 . . . . 5  class  ( Base `  w )
85cv 1373 . . . . . . 7  class  x
9 cip 14551 . . . . . . . 8  class  .i
104, 9cfv 5581 . . . . . . 7  class  ( .i
`  w )
118, 8, 10co 6277 . . . . . 6  class  ( x ( .i `  w
) x )
12 csqr 13018 . . . . . 6  class  sqr
1311, 12cfv 5581 . . . . 5  class  ( sqr `  ( x ( .i
`  w ) x ) )
145, 7, 13cmpt 4500 . . . 4  class  ( x  e.  ( Base `  w
)  |->  ( sqr `  (
x ( .i `  w ) x ) ) )
15 ctng 20829 . . . 4  class toNrmGrp
164, 14, 15co 6277 . . 3  class  ( w toNrmGrp  ( x  e.  ( Base `  w )  |->  ( sqr `  ( x ( .i `  w
) x ) ) ) )
172, 3, 16cmpt 4500 . 2  class  ( w  e.  _V  |->  ( w toNrmGrp  ( x  e.  ( Base `  w )  |->  ( sqr `  ( x ( .i `  w
) x ) ) ) ) )
181, 17wceq 1374 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  21391
  Copyright terms: Public domain W3C validator