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

Definition df-tch 18621
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 18619 . 2  class toCHil
2 vw . . 3  set  w
3 cvv 2801 . . 3  class  _V
42cv 1631 . . . 4  class  w
5 vx . . . . 5  set  x
6 cbs 13164 . . . . . 6  class  Base
74, 6cfv 5271 . . . . 5  class  ( Base `  w )
85cv 1631 . . . . . . 7  class  x
9 cip 13229 . . . . . . . 8  class  .i
104, 9cfv 5271 . . . . . . 7  class  ( .i
`  w )
118, 8, 10co 5874 . . . . . 6  class  ( x ( .i `  w
) x )
12 csqr 11734 . . . . . 6  class  sqr
1311, 12cfv 5271 . . . . 5  class  ( sqr `  ( x ( .i
`  w ) x ) )
145, 7, 13cmpt 4093 . . . 4  class  ( x  e.  ( Base `  w
)  |->  ( sqr `  (
x ( .i `  w ) x ) ) )
15 ctng 18117 . . . 4  class toNrmGrp
164, 14, 15co 5874 . . 3  class  ( w toNrmGrp  ( x  e.  ( Base `  w )  |->  ( sqr `  ( x ( .i `  w
) x ) ) ) )
172, 3, 16cmpt 4093 . 2  class  ( w  e.  _V  |->  ( w toNrmGrp  ( x  e.  ( Base `  w )  |->  ( sqr `  ( x ( .i `  w
) x ) ) ) ) )
181, 17wceq 1632 1  wff toCHil  =  ( w  e.  _V  |->  ( w toNrmGrp  ( x  e.  ( Base `  w
)  |->  ( sqr `  (
x ( .i `  w ) x ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  tchval  18666
  Copyright terms: Public domain W3C validator