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 ⊢ toCPreHil = w ∈ V ⟼ w toNrmGrp x ∈ Base w ⟼ x ⋅ 𝑖 ⁡ w x

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctcph class toCPreHil
1 vw setvar w
2 cvv class V
3 1 cv setvar w
4 ctng class toNrmGrp
5 vx setvar x
6 cbs class Base
7 3 6 cfv class Base w
8 csqrt class √
9 5 cv setvar x
10 cip class ⋅ 𝑖
11 3 10 cfv class ⋅ 𝑖 ⁡ w
12 9 9 11 co class x ⋅ 𝑖 ⁡ w x
13 12 8 cfv class x ⋅ 𝑖 ⁡ w x
14 5 7 13 cmpt class x ∈ Base w ⟼ x ⋅ 𝑖 ⁡ w x
15 3 14 4 co class w toNrmGrp x ∈ Base w ⟼ x ⋅ 𝑖 ⁡ w x
16 1 2 15 cmpt class w ∈ V ⟼ w toNrmGrp x ∈ Base w ⟼ x ⋅ 𝑖 ⁡ w x
17 0 16 wceq wff toCPreHil = w ∈ V ⟼ w toNrmGrp x ∈ Base w ⟼ x ⋅ 𝑖 ⁡ w x