Definition df-tcph

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 (see tcphcph ). (Contributed by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Assertion	df-tcph	$$⊢\mathrm{toCPreHil}=\left(w\in \mathrm{V}⟼w\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctcph	$$class\mathrm{toCPreHil}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarw$$
4		ctng	$$class\mathrm{toNrmGrp}$$
5		vx	$$setvarx$$
6		cbs	$$class\mathrm{Base}$$
7	3 6	cfv	$$class{\mathrm{Base}}_w$$
8		csqrt	$$class\surd$$
9	5	cv	$$setvarx$$
10		cip	$$class{\cdot }_{𝑖}$$
11	3 10	cfv	$$class{\cdot }_{𝑖}\left(w\right)$$
12	9 9 11	co	$$class\left(x{\cdot }_{𝑖}\left(w\right)x\right)$$
13	12 8	cfv	$$class\sqrt{x{\cdot }_{𝑖}\left(w\right)x}$$
14	5 7 13	cmpt	$$class\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)$$
15	3 14 4	co	$$class\left(w\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)\right)$$
16	1 2 15	cmpt	$$class\left(w\in \mathrm{V}⟼w\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)\right)$$
17	0 16	wceq	$$wff\mathrm{toCPreHil}=\left(w\in \mathrm{V}⟼w\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)\right)$$