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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctcph	⊢ toℂPreHil
1		vw	⊢ 𝑤
2		cvv	⊢ V
3	1	cv	⊢ 𝑤
4		ctng	⊢ toNrmGrp
5		vx	⊢ 𝑥
6		cbs	⊢ Base
7	3 6	cfv	⊢ ( Base ‘ 𝑤 )
8		csqrt	⊢ √
9	5	cv	⊢ 𝑥
10		cip	⊢ ·𝑖
11	3 10	cfv	⊢ ( ·𝑖 ‘ 𝑤 )
12	9 9 11	co	⊢ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 )
13	12 8	cfv	⊢ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) )
14	5 7 13	cmpt	⊢ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) )
15	3 14 4	co	⊢ ( 𝑤 toNrmGrp ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) )
16	1 2 15	cmpt	⊢ ( 𝑤 ∈ V ↦ ( 𝑤 toNrmGrp ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) ) )
17	0 16	wceq	⊢ toℂPreHil = ( 𝑤 ∈ V ↦ ( 𝑤 toNrmGrp ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) ) )