Definition df-tcph 24686

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

Assertion

Ref	Expression
df-tcph	⊢ toℂPreHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))))

Distinct variable group:   𝑥,𝑤

Detailed syntax breakdown of Definition df-tcph

Step	Hyp	Ref	Expression
1		ctcph 24684	. 2 class toℂPreHil
2		vw	. . 3 setvar 𝑤
3		cvv 3475	. . 3 class V
4	2	cv 1541	. . . 4 class 𝑤
5		vx	. . . . 5 setvar 𝑥
6		cbs 17144	. . . . . 6 class Base
7	4, 6	cfv 6544	. . . . 5 class (Base‘𝑤)
8	5	cv 1541	. . . . . . 7 class 𝑥
9		cip 17202	. . . . . . . 8 class ·𝑖
10	4, 9	cfv 6544	. . . . . . 7 class (·𝑖‘𝑤)
11	8, 8, 10	co 7409	. . . . . 6 class (𝑥(·𝑖‘𝑤)𝑥)
12		csqrt 15180	. . . . . 6 class √
13	11, 12	cfv 6544	. . . . 5 class (√‘(𝑥(·𝑖‘𝑤)𝑥))
14	5, 7, 13	cmpt 5232	. . . 4 class (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))
15		ctng 24087	. . . 4 class toNrmGrp
16	4, 14, 15	co 7409	. . 3 class (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))
17	2, 3, 16	cmpt 5232	. 2 class (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))))
18	1, 17	wceq 1542	1 wff toℂPreHil = (𝑤 ∈ V ↦ (𝑤 toNrmGrp (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))))

This definition is referenced by:  tcphval  24735