Metamath Proof Explorer


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 ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖𝑤 ) 𝑥 ) ) ) ) )