Definition df-cph 22968

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

Assertion

Ref	Expression
df-cph	|- CPreHil = { w e. ( PreHil i^i NrmMod ) | [. (Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ ( sqr " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) ) }

Distinct variable group:   f, k, w, x

Detailed syntax breakdown of Definition df-cph

Step	Hyp	Ref	Expression
1		ccph 22966	. 2 class CPreHil
2		vf	. . . . . . . 8 setvar f
3	2	cv 1482	. . . . . . 7 class f
4		ccnfld 19746	. . . . . . . 8 class ℂfld
5		vk	. . . . . . . . 9 setvar k
6	5	cv 1482	. . . . . . . 8 class k
7		cress 15858	. . . . . . . 8 class ↾s
8	4, 6, 7	co 6650	. . . . . . 7 class (ℂfld ↾s k )
9	3, 8	wceq 1483	. . . . . 6 wff f = (ℂfld ↾s k )
10		csqrt 13973	. . . . . . . 8 class sqr
11		cc0 9936	. . . . . . . . . 10 class 0
12		cpnf 10071	. . . . . . . . . 10 class +oo
13		cico 12177	. . . . . . . . . 10 class [,)
14	11, 12, 13	co 6650	. . . . . . . . 9 class ( 0 [,) +oo )
15	6, 14	cin 3573	. . . . . . . 8 class ( k i^i ( 0 [,) +oo ) )
16	10, 15	cima 5117	. . . . . . 7 class ( sqr " ( k i^i ( 0 [,) +oo ) ) )
17	16, 6	wss 3574	. . . . . 6 wff ( sqr " ( k i^i ( 0 [,) +oo ) ) ) C_ k
18		vw	. . . . . . . . 9 setvar w
19	18	cv 1482	. . . . . . . 8 class w
20		cnm 22381	. . . . . . . 8 class norm
21	19, 20	cfv 5888	. . . . . . 7 class ( norm ` w )
22		vx	. . . . . . . 8 setvar x
23		cbs 15857	. . . . . . . . 9 class Base
24	19, 23	cfv 5888	. . . . . . . 8 class ( Base ` w )
25	22	cv 1482	. . . . . . . . . 10 class x
26		cip 15946	. . . . . . . . . . 11 class .i
27	19, 26	cfv 5888	. . . . . . . . . 10 class ( .i ` w )
28	25, 25, 27	co 6650	. . . . . . . . 9 class ( x ( .i ` w ) x )
29	28, 10	cfv 5888	. . . . . . . 8 class ( sqr ` ( x ( .i ` w ) x ) )
30	22, 24, 29	cmpt 4729	. . . . . . 7 class ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) )
31	21, 30	wceq 1483	. . . . . 6 wff ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) )
32	9, 17, 31	w3a 1037	. . . . 5 wff ( f = (ℂfld ↾s k ) /\ ( sqr " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) )
33	3, 23	cfv 5888	. . . . 5 class ( Base ` f )
34	32, 5, 33	wsbc 3435	. . . 4 wff [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ ( sqr " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) )
35		csca 15944	. . . . 5 class Scalar
36	19, 35	cfv 5888	. . . 4 class (Scalar ` w )
37	34, 2, 36	wsbc 3435	. . 3 wff [. (Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ ( sqr " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) )
38		cphl 19969	. . . 4 class PreHil
39		cnlm 22385	. . . 4 class NrmMod
40	38, 39	cin 3573	. . 3 class ( PreHil i^i NrmMod )
41	37, 18, 40	crab 2916	. 2 class { w e. ( PreHil i^i NrmMod ) | [. (Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ ( sqr " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) ) }
42	1, 41	wceq 1483	1 wff CPreHil = { w e. ( PreHil i^i NrmMod ) | [. (Scalar ` w ) / f ]. [. ( Base ` f ) / k ]. ( f = (ℂfld ↾s k ) /\ ( sqr " ( k i^i ( 0 [,) +oo ) ) ) C_ k /\ ( norm ` w ) = ( x e. ( Base ` w ) |-> ( sqr ` ( x ( .i ` w ) x ) ) ) ) }

This definition is referenced by:  iscph  22970