Definition df-cph 23775

Description: Define the class of subcomplex pre-Hilbert spaces. By restricting the scalar field to a subfield of ℂ_fld 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.)

Assertion

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

Distinct variable group:   𝑓,𝑘,𝑤,𝑥

Detailed syntax breakdown of Definition df-cph

Step	Hyp	Ref	Expression
1		ccph 23773	. 2 class ℂPreHil
2		vf	. . . . . . . 8 setvar 𝑓
3	2	cv 1535	. . . . . . 7 class 𝑓
4		ccnfld 20548	. . . . . . . 8 class ℂfld
5		vk	. . . . . . . . 9 setvar 𝑘
6	5	cv 1535	. . . . . . . 8 class 𝑘
7		cress 16487	. . . . . . . 8 class ↾s
8	4, 6, 7	co 7159	. . . . . . 7 class (ℂfld ↾s 𝑘)
9	3, 8	wceq 1536	. . . . . 6 wff 𝑓 = (ℂfld ↾s 𝑘)
10		csqrt 14595	. . . . . . . 8 class √
11		cc0 10540	. . . . . . . . . 10 class 0
12		cpnf 10675	. . . . . . . . . 10 class +∞
13		cico 12743	. . . . . . . . . 10 class [,)
14	11, 12, 13	co 7159	. . . . . . . . 9 class (0[,)+∞)
15	6, 14	cin 3938	. . . . . . . 8 class (𝑘 ∩ (0[,)+∞))
16	10, 15	cima 5561	. . . . . . 7 class (√ “ (𝑘 ∩ (0[,)+∞)))
17	16, 6	wss 3939	. . . . . 6 wff (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘
18		vw	. . . . . . . . 9 setvar 𝑤
19	18	cv 1535	. . . . . . . 8 class 𝑤
20		cnm 23189	. . . . . . . 8 class norm
21	19, 20	cfv 6358	. . . . . . 7 class (norm‘𝑤)
22		vx	. . . . . . . 8 setvar 𝑥
23		cbs 16486	. . . . . . . . 9 class Base
24	19, 23	cfv 6358	. . . . . . . 8 class (Base‘𝑤)
25	22	cv 1535	. . . . . . . . . 10 class 𝑥
26		cip 16573	. . . . . . . . . . 11 class ·𝑖
27	19, 26	cfv 6358	. . . . . . . . . 10 class (·𝑖‘𝑤)
28	25, 25, 27	co 7159	. . . . . . . . 9 class (𝑥(·𝑖‘𝑤)𝑥)
29	28, 10	cfv 6358	. . . . . . . 8 class (√‘(𝑥(·𝑖‘𝑤)𝑥))
30	22, 24, 29	cmpt 5149	. . . . . . 7 class (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))
31	21, 30	wceq 1536	. . . . . 6 wff (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))
32	9, 17, 31	w3a 1083	. . . . 5 wff (𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))
33	3, 23	cfv 6358	. . . . 5 class (Base‘𝑓)
34	32, 5, 33	wsbc 3775	. . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))
35		csca 16571	. . . . 5 class Scalar
36	19, 35	cfv 6358	. . . 4 class (Scalar‘𝑤)
37	34, 2, 36	wsbc 3775	. . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))
38		cphl 20771	. . . 4 class PreHil
39		cnlm 23193	. . . 4 class NrmMod
40	38, 39	cin 3938	. . 3 class (PreHil ∩ NrmMod)
41	37, 18, 40	crab 3145	. 2 class {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))}
42	1, 41	wceq 1536	1 wff ℂPreHil = {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))}

This definition is referenced by:  iscph  23777