Definition df-tch 22969

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 subcomplex 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

Step	Hyp	Ref	Expression
1		ctch 22967	. 2 class toCHil
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . 4 class w
5		vx	. . . . 5 setvar x
6		cbs 15857	. . . . . 6 class Base
7	4, 6	cfv 5888	. . . . 5 class ( Base ` w )
8	5	cv 1482	. . . . . . 7 class x
9		cip 15946	. . . . . . . 8 class .i
10	4, 9	cfv 5888	. . . . . . 7 class ( .i ` w )
11	8, 8, 10	co 6650	. . . . . 6 class ( x ( .i ` w ) x )
12		csqrt 13973	. . . . . 6 class sqr
13	11, 12	cfv 5888	. . . . 5 class ( sqr ` ( x ( .i ` w ) x ) )
14	5, 7, 13	cmpt 4729	. . . 4 class ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) )
15		ctng 22383	. . . 4 class toNrmGrp
16	4, 14, 15	co 6650	. . 3 class ( w toNrmGrp ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) )
17	2, 3, 16	cmpt 4729	. 2 class ( w e. _V |-> ( w toNrmGrp ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) ) )
18	1, 17	wceq 1483	1 wff toCHil = ( w e. _V |-> ( w toNrmGrp ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) ) )

This definition is referenced by:  tchval  23017