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	$$⊢\mathrm{CPreHil}=\left\{w\in \left(\mathrm{PreHil}\cap \mathrm{NrmMod}\right)|\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\left(f={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}k\wedge \surd \left[k\cap \left[0,\mathrm{+\infty }\right)\right]\subseteq k\wedge \mathrm{norm}\left(w\right)=\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccph	$$class\mathrm{CPreHil}$$
1		vw	$$setvarw$$
2		cphl	$$class\mathrm{PreHil}$$
3		cnlm	$$class\mathrm{NrmMod}$$
4	2 3	cin	$$class\left(\mathrm{PreHil}\cap \mathrm{NrmMod}\right)$$
5		csca	$$class\mathrm{Scalar}$$
6	1	cv	$$setvarw$$
7	6 5	cfv	$$class\mathrm{Scalar}\left(w\right)$$
8		vf	$$setvarf$$
9		cbs	$$class\mathrm{Base}$$
10	8	cv	$$setvarf$$
11	10 9	cfv	$$class{\mathrm{Base}}_f$$
12		vk	$$setvark$$
13		ccnfld	$$class{ℂ}_{\mathrm{fld}}$$
14		cress	$$class{\upharpoonright }_{𝑠}$$
15	12	cv	$$setvark$$
16	13 15 14	co	$$class\left({ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}k\right)$$
17	10 16	wceq	$$wfff={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}k$$
18		csqrt	$$class\surd$$
19		cc0	$$class0$$
20		cico	$$class\left[.\right)$$
21		cpnf	$$class\mathrm{+\infty }$$
22	19 21 20	co	$$class\left[0,\mathrm{+\infty }\right)$$
23	15 22	cin	$$class\left(k\cap \left[0,\mathrm{+\infty }\right)\right)$$
24	18 23	cima	$$class\surd \left[k\cap \left[0,\mathrm{+\infty }\right)\right]$$
25	24 15	wss	$$wff\surd \left[k\cap \left[0,\mathrm{+\infty }\right)\right]\subseteq k$$
26		cnm	$$class\mathrm{norm}$$
27	6 26	cfv	$$class\mathrm{norm}\left(w\right)$$
28		vx	$$setvarx$$
29	6 9	cfv	$$class{\mathrm{Base}}_w$$
30	28	cv	$$setvarx$$
31		cip	$$class{\cdot }_{𝑖}$$
32	6 31	cfv	$$class{\cdot }_{𝑖}\left(w\right)$$
33	30 30 32	co	$$class\left(x{\cdot }_{𝑖}\left(w\right)x\right)$$
34	33 18	cfv	$$class\sqrt{x{\cdot }_{𝑖}\left(w\right)x}$$
35	28 29 34	cmpt	$$class\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)$$
36	27 35	wceq	$$wff\mathrm{norm}\left(w\right)=\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)$$
37	17 25 36	w3a	$$wff\left(f={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}k\wedge \surd \left[k\cap \left[0,\mathrm{+\infty }\right)\right]\subseteq k\wedge \mathrm{norm}\left(w\right)=\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)\right)$$
38	37 12 11	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\left(f={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}k\wedge \surd \left[k\cap \left[0,\mathrm{+\infty }\right)\right]\subseteq k\wedge \mathrm{norm}\left(w\right)=\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)\right)$$
39	38 8 7	wsbc	$$wff\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\left(f={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}k\wedge \surd \left[k\cap \left[0,\mathrm{+\infty }\right)\right]\subseteq k\wedge \mathrm{norm}\left(w\right)=\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)\right)$$
40	39 1 4	crab	$$class\left\{w\in \left(\mathrm{PreHil}\cap \mathrm{NrmMod}\right)|\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\left(f={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}k\wedge \surd \left[k\cap \left[0,\mathrm{+\infty }\right)\right]\subseteq k\wedge \mathrm{norm}\left(w\right)=\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)\right)\right\}$$
41	0 40	wceq	$$wff\mathrm{CPreHil}=\left\{w\in \left(\mathrm{PreHil}\cap \mathrm{NrmMod}\right)|\underset{\dot{}}{[}\mathrm{Scalar}\left(w\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\left(f={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}k\wedge \surd \left[k\cap \left[0,\mathrm{+\infty }\right)\right]\subseteq k\wedge \mathrm{norm}\left(w\right)=\left(x\in {\mathrm{Base}}_w⟼\sqrt{x{\cdot }_{𝑖}\left(w\right)x}\right)\right)\right\}$$