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

Metamath Proof Explorer

Definition df-cph

Description: Define the class of subcomplex pre-Hilbert spaces. By restricting the scalar field to a subfield of CCfld closed under square roots of nonnegative reals, we have enough structure to define a norm, with the associated connection to a metric and topology. (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Assertion df-cph ℂPreHil = { 𝑤 ∈ ( PreHil ∩ NrmMod ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝑘 ∧ ( norm ‘ 𝑤 ) = ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccph ⊢ ℂPreHil
1 vw ⊢ 𝑤
2 cphl ⊢ PreHil
3 cnlm ⊢ NrmMod
4 2 3 cin ⊢ ( PreHil ∩ NrmMod )
5 csca ⊢ Scalar
6 1 cv ⊢ 𝑤
7 6 5 cfv ⊢ ( Scalar ‘ 𝑤 )
8 vf ⊢ 𝑓
9 cbs ⊢ Base
10 8 cv ⊢ 𝑓
11 10 9 cfv ⊢ ( Base ‘ 𝑓 )
12 vk ⊢ 𝑘
13 ccnfld ⊢ ℂfld
14 cress ⊢ ↾s
15 12 cv ⊢ 𝑘
16 13 15 14 co ⊢ ( ℂfld ↾s 𝑘 )
17 10 16 wceq ⊢ 𝑓 = ( ℂfld ↾s 𝑘 )
18 csqrt ⊢ √
19 cc0 ⊢ 0
20 cico ⊢ [,)
21 cpnf ⊢ +∞
22 19 21 20 co ⊢ ( 0 [,) +∞ )
23 15 22 cin ⊢ ( 𝑘 ∩ ( 0 [,) +∞ ) )
24 18 23 cima ⊢ ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) )
25 24 15 wss ⊢ ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝑘
26 cnm ⊢ norm
27 6 26 cfv ⊢ ( norm ‘ 𝑤 )
28 vx ⊢ 𝑥
29 6 9 cfv ⊢ ( Base ‘ 𝑤 )
30 28 cv ⊢ 𝑥
31 cip ⊢ ·𝑖
32 6 31 cfv ⊢ ( ·𝑖 ‘ 𝑤 )
33 30 30 32 co ⊢ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 )
34 33 18 cfv ⊢ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) )
35 28 29 34 cmpt ⊢ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) )
36 27 35 wceq ⊢ ( norm ‘ 𝑤 ) = ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) )
37 17 25 36 w3a ⊢ ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝑘 ∧ ( norm ‘ 𝑤 ) = ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) )
38 37 12 11 wsbc ⊢ [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝑘 ∧ ( norm ‘ 𝑤 ) = ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) )
39 38 8 7 wsbc ⊢ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝑘 ∧ ( norm ‘ 𝑤 ) = ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) )
40 39 1 4 crab ⊢ { 𝑤 ∈ ( PreHil ∩ NrmMod ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝑘 ∧ ( norm ‘ 𝑤 ) = ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) ) }
41 0 40 wceq ⊢ ℂPreHil = { 𝑤 ∈ ( PreHil ∩ NrmMod ) ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ ( √ “ ( 𝑘 ∩ ( 0 [,) +∞ ) ) ) ⊆ 𝑘 ∧ ( norm ‘ 𝑤 ) = ( 𝑥 ∈ ( Base ‘ 𝑤 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑤 ) 𝑥 ) ) ) ) }