Definition df-cph 24685

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 24683	. 2 class ℂPreHil
2		vf	. . . . . . . 8 setvar 𝑓
3	2	cv 1541	. . . . . . 7 class 𝑓
4		ccnfld 20944	. . . . . . . 8 class ℂfld
5		vk	. . . . . . . . 9 setvar 𝑘
6	5	cv 1541	. . . . . . . 8 class 𝑘
7		cress 17173	. . . . . . . 8 class ↾s
8	4, 6, 7	co 7409	. . . . . . 7 class (ℂfld ↾s 𝑘)
9	3, 8	wceq 1542	. . . . . 6 wff 𝑓 = (ℂfld ↾s 𝑘)
10		csqrt 15180	. . . . . . . 8 class √
11		cc0 11110	. . . . . . . . . 10 class 0
12		cpnf 11245	. . . . . . . . . 10 class +∞
13		cico 13326	. . . . . . . . . 10 class [,)
14	11, 12, 13	co 7409	. . . . . . . . 9 class (0[,)+∞)
15	6, 14	cin 3948	. . . . . . . 8 class (𝑘 ∩ (0[,)+∞))
16	10, 15	cima 5680	. . . . . . 7 class (√ “ (𝑘 ∩ (0[,)+∞)))
17	16, 6	wss 3949	. . . . . 6 wff (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘
18		vw	. . . . . . . . 9 setvar 𝑤
19	18	cv 1541	. . . . . . . 8 class 𝑤
20		cnm 24085	. . . . . . . 8 class norm
21	19, 20	cfv 6544	. . . . . . 7 class (norm‘𝑤)
22		vx	. . . . . . . 8 setvar 𝑥
23		cbs 17144	. . . . . . . . 9 class Base
24	19, 23	cfv 6544	. . . . . . . 8 class (Base‘𝑤)
25	22	cv 1541	. . . . . . . . . 10 class 𝑥
26		cip 17202	. . . . . . . . . . 11 class ·𝑖
27	19, 26	cfv 6544	. . . . . . . . . 10 class (·𝑖‘𝑤)
28	25, 25, 27	co 7409	. . . . . . . . 9 class (𝑥(·𝑖‘𝑤)𝑥)
29	28, 10	cfv 6544	. . . . . . . 8 class (√‘(𝑥(·𝑖‘𝑤)𝑥))
30	22, 24, 29	cmpt 5232	. . . . . . 7 class (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))
31	21, 30	wceq 1542	. . . . . 6 wff (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥)))
32	9, 17, 31	w3a 1088	. . . . 5 wff (𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))
33	3, 23	cfv 6544	. . . . 5 class (Base‘𝑓)
34	32, 5, 33	wsbc 3778	. . . 4 wff [(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))
35		csca 17200	. . . . 5 class Scalar
36	19, 35	cfv 6544	. . . 4 class (Scalar‘𝑤)
37	34, 2, 36	wsbc 3778	. . 3 wff [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))
38		cphl 21177	. . . 4 class PreHil
39		cnlm 24089	. . . 4 class NrmMod
40	38, 39	cin 3948	. . 3 class (PreHil ∩ NrmMod)
41	37, 18, 40	crab 3433	. 2 class {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))}
42	1, 41	wceq 1542	1 wff ℂPreHil = {𝑤 ∈ (PreHil ∩ NrmMod) ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s 𝑘) ∧ (√ “ (𝑘 ∩ (0[,)+∞))) ⊆ 𝑘 ∧ (norm‘𝑤) = (𝑥 ∈ (Base‘𝑤) ↦ (√‘(𝑥(·𝑖‘𝑤)𝑥))))}

This definition is referenced by:  iscph  24687