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	⊢ toℂHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))))

Distinct variable group:   𝑥,𝑤

Detailed syntax breakdown of Definition df-tch

Step	Hyp	Ref	Expression
1		ctch 22967	. 2 class toℂHil
2		vw	. . 3 setvar 𝑤
3		cvv 3200	. . 3 class V
4	2	cv 1482	. . . 4 class 𝑤
5		vx	. . . . 5 setvar 𝑥
6		cbs 15857	. . . . . 6 class Base
7	4, 6	cfv 5888	. . . . 5 class (Base‘𝑤)
8	5	cv 1482	. . . . . . 7 class 𝑥
9		cip 15946	. . . . . . . 8 class ·𝑖
10	4, 9	cfv 5888	. . . . . . 7 class (·𝑖‘𝑤)
11	8, 8, 10	co 6650	. . . . . 6 class (𝑥(·𝑖‘𝑤)𝑥)
12		csqrt 13973	. . . . . 6 class √
13	11, 12	cfv 5888	. . . . 5 class (√‘(𝑥(·𝑖‘𝑤)𝑥))
14	5, 7, 13	cmpt 4729	. . . 4 class (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))
15		ctng 22383	. . . 4 class toNrmGrp
16	4, 14, 15	co 6650	. . 3 class (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))
17	2, 3, 16	cmpt 4729	. 2 class (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))))
18	1, 17	wceq 1483	1 wff toℂHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))))

This definition is referenced by:  tchval  23017