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

Definition df-tch 19124
 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 19122 . 2 toCHil
2 vw . . 3
3 cvv 2948 . . 3
42cv 1651 . . . 4
5 vx . . . . 5
6 cbs 13461 . . . . . 6
74, 6cfv 5446 . . . . 5
85cv 1651 . . . . . . 7
9 cip 13526 . . . . . . . 8
104, 9cfv 5446 . . . . . . 7
118, 8, 10co 6073 . . . . . 6
12 csqr 12030 . . . . . 6
1311, 12cfv 5446 . . . . 5
145, 7, 13cmpt 4258 . . . 4
15 ctng 18618 . . . 4 toNrmGrp
164, 14, 15co 6073 . . 3 toNrmGrp
172, 3, 16cmpt 4258 . 2 toNrmGrp
181, 17wceq 1652 1 toCHil toNrmGrp
 Colors of variables: wff set class This definition is referenced by:  tchval  19169
 Copyright terms: Public domain W3C validator