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