This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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