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 toNrmGrp
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-tch
StepHypRef Expression
1 ctch 21344 . 2 toCHil
2 vw . . 3
3 cvv 3108 . . 3
42cv 1373 . . . 4
5 vx . . . . 5
6 cbs 14481 . . . . . 6
74, 6cfv 5581 . . . . 5
85cv 1373 . . . . . . 7
9 cip 14551 . . . . . . . 8
104, 9cfv 5581 . . . . . . 7
118, 8, 10co 6277 . . . . . 6
12 csqr 13018 . . . . . 6
1311, 12cfv 5581 . . . . 5
145, 7, 13cmpt 4500 . . . 4
15 ctng 20829 . . . 4 toNrmGrp
164, 14, 15co 6277 . . 3 toNrmGrp
172, 3, 16cmpt 4500 . 2 toNrmGrp
181, 17wceq 1374 1 toCHil toNrmGrp
 Colors of variables: wff setvar class This definition is referenced by:  tchval  21391
 Copyright terms: Public domain W3C validator