Definition df-cph 25202

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 25200	. 2 class ℂPreHil
2		vf	. . . . . . . 8 setvar 𝑓
3	2	cv 1539	. . . . . . 7 class 𝑓
4		ccnfld 21364	. . . . . . . 8 class ℂfld
5		vk	. . . . . . . . 9 setvar 𝑘
6	5	cv 1539	. . . . . . . 8 class 𝑘
7		cress 17274	. . . . . . . 8 class ↾s
8	4, 6, 7	co 7431	. . . . . . 7 class (ℂfld ↾s 𝑘)
9	3, 8	wceq 1540	. . . . . 6 wff 𝑓 = (ℂfld ↾s 𝑘)
10		csqrt 15272	. . . . . . . 8 class √
11		cc0 11155	. . . . . . . . . 10 class 0
12		cpnf 11292	. . . . . . . . . 10 class +∞
13		cico 13389	. . . . . . . . . 10 class [,)
14	11, 12, 13	co 7431	. . . . . . . . 9 class (0[,)+∞)
15	6, 14	cin 3950	. . . . . . . 8 class (𝑘 ∩ (0[,)+∞))
16	10, 15	cima 5688	. . . . . . 7 class (√ “ (𝑘 ∩ (0[,)+∞)))
17	16, 6	wss 3951	. . . . . 6 wff (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘
18		vw	. . . . . . . . 9 setvar 𝑤
19	18	cv 1539	. . . . . . . 8 class 𝑤
20		cnm 24589	. . . . . . . 8 class norm
21	19, 20	cfv 6561	. . . . . . 7 class (norm‘𝑤)
22		vx	. . . . . . . 8 setvar 𝑥
23		cbs 17247	. . . . . . . . 9 class Base
24	19, 23	cfv 6561	. . . . . . . 8 class (Base‘𝑤)
25	22	cv 1539	. . . . . . . . . 10 class 𝑥
26		cip 17302	. . . . . . . . . . 11 class ·𝑖
27	19, 26	cfv 6561	. . . . . . . . . 10 class (·𝑖‘𝑤)
28	25, 25, 27	co 7431	. . . . . . . . 9 class (𝑥(·𝑖‘𝑤)𝑥)
29	28, 10	cfv 6561	. . . . . . . 8 class (√‘(𝑥(·𝑖‘𝑤)𝑥))
30	22, 24, 29	cmpt 5225	. . . . . . 7 class (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))
31	21, 30	wceq 1540	. . . . . 6 wff (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))
32	9, 17, 31	w3a 1087	. . . . 5 wff (𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))
33	3, 23	cfv 6561	. . . . 5 class (Base‘𝑓)
34	32, 5, 33	wsbc 3788	. . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))
35		csca 17300	. . . . 5 class Scalar
36	19, 35	cfv 6561	. . . 4 class (Scalar‘𝑤)
37	34, 2, 36	wsbc 3788	. . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))
38		cphl 21642	. . . 4 class PreHil
39		cnlm 24593	. . . 4 class NrmMod
40	38, 39	cin 3950	. . 3 class (PreHil ∩ NrmMod)
41	37, 18, 40	crab 3436	. 2 class {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))}
42	1, 41	wceq 1540	1 wff ℂPreHil = {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))}

This definition is referenced by:  iscph  25204