ishl2

Description: A Hilbert space is a complete subcomplex pre-Hilbert space over RR or CC . (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Hypotheses	hlress.f	$⊢ F = Scalar (W)$
	hlress.k	$⊢ K = {Base}_{F}$
Assertion	ishl2	$⊢ W \in ℂHil \leftrightarrow (W \in CMetSp \land W \in CPreHil \land K \in \{ℝ, ℂ\})$

Proof

Step	Hyp	Ref	Expression
1		hlress.f	$⊢ F = Scalar (W)$
2		hlress.k	$⊢ K = {Base}_{F}$
3		ishl	$⊢ W \in ℂHil \leftrightarrow (W \in Ban \land W \in CPreHil)$
4		df-3an	$⊢ (W \in CMetSp \land K \in \{ℝ, ℂ\} \land W \in CPreHil) \leftrightarrow ((W \in CMetSp \land K \in \{ℝ, ℂ\}) \land W \in CPreHil)$
5		3ancomb	$⊢ (W \in CMetSp \land W \in CPreHil \land K \in \{ℝ, ℂ\}) \leftrightarrow (W \in CMetSp \land K \in \{ℝ, ℂ\} \land W \in CPreHil)$
6		cphnvc	$⊢ W \in CPreHil \to W \in NrmVec$
7	1	isbn	$⊢ W \in Ban \leftrightarrow (W \in NrmVec \land W \in CMetSp \land F \in CMetSp)$
8		3anass	$⊢ (W \in NrmVec \land W \in CMetSp \land F \in CMetSp) \leftrightarrow (W \in NrmVec \land (W \in CMetSp \land F \in CMetSp))$
9	7 8	bitri	$⊢ W \in Ban \leftrightarrow (W \in NrmVec \land (W \in CMetSp \land F \in CMetSp))$
10	9	baib	$⊢ W \in NrmVec \to (W \in Ban \leftrightarrow (W \in CMetSp \land F \in CMetSp))$
11	6 10	syl	$⊢ W \in CPreHil \to (W \in Ban \leftrightarrow (W \in CMetSp \land F \in CMetSp))$
12	1 2	cphsca	$⊢ W \in CPreHil \to F = ℂ_{fld} ↾_{𝑠} K$
13	12	eleq1d	$⊢ W \in CPreHil \to (F \in CMetSp \leftrightarrow ℂ_{fld} ↾_{𝑠} K \in CMetSp)$
14	1 2	cphsubrg	$⊢ W \in CPreHil \to K \in SubRing (ℂ_{fld})$
15		cphlvec	$⊢ W \in CPreHil \to W \in LVec$
16	1	lvecdrng	$⊢ W \in LVec \to F \in DivRing$
17	15 16	syl	$⊢ W \in CPreHil \to F \in DivRing$
18	12 17	eqeltrrd	$⊢ W \in CPreHil \to ℂ_{fld} ↾_{𝑠} K \in DivRing$
19		eqid	$⊢ ℂ_{fld} ↾_{𝑠} K = ℂ_{fld} ↾_{𝑠} K$
20	19	cncdrg	$⊢ (K \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} K \in DivRing \land ℂ_{fld} ↾_{𝑠} K \in CMetSp) \to K \in \{ℝ, ℂ\}$
21	20	3expia	$⊢ (K \in SubRing (ℂ_{fld}) \land ℂ_{fld} ↾_{𝑠} K \in DivRing) \to (ℂ_{fld} ↾_{𝑠} K \in CMetSp \to K \in \{ℝ, ℂ\})$
22	14 18 21	syl2anc	$⊢ W \in CPreHil \to (ℂ_{fld} ↾_{𝑠} K \in CMetSp \to K \in \{ℝ, ℂ\})$
23		elpri	$⊢ K \in \{ℝ, ℂ\} \to (K = ℝ \lor K = ℂ)$
24		oveq2	$⊢ K = ℝ \to ℂ_{fld} ↾_{𝑠} K = ℂ_{fld} ↾_{𝑠} ℝ$
25		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
26	25	recld2	$⊢ ℝ \in Clsd (TopOpen (ℂ_{fld}))$
27		cncms	$⊢ ℂ_{fld} \in CMetSp$
28		ax-resscn	$⊢ ℝ \subseteq ℂ$
29		eqid	$⊢ ℂ_{fld} ↾_{𝑠} ℝ = ℂ_{fld} ↾_{𝑠} ℝ$
30		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
31	29 30 25	cmsss	$⊢ (ℂ_{fld} \in CMetSp \land ℝ \subseteq ℂ) \to (ℂ_{fld} ↾_{𝑠} ℝ \in CMetSp \leftrightarrow ℝ \in Clsd (TopOpen (ℂ_{fld})))$
32	27 28 31	mp2an	$⊢ ℂ_{fld} ↾_{𝑠} ℝ \in CMetSp \leftrightarrow ℝ \in Clsd (TopOpen (ℂ_{fld}))$
33	26 32	mpbir	$⊢ ℂ_{fld} ↾_{𝑠} ℝ \in CMetSp$
34	24 33	eqeltrdi	$⊢ K = ℝ \to ℂ_{fld} ↾_{𝑠} K \in CMetSp$
35		oveq2	$⊢ K = ℂ \to ℂ_{fld} ↾_{𝑠} K = ℂ_{fld} ↾_{𝑠} ℂ$
36	30	ressid	$⊢ ℂ_{fld} \in CMetSp \to ℂ_{fld} ↾_{𝑠} ℂ = ℂ_{fld}$
37	27 36	ax-mp	$⊢ ℂ_{fld} ↾_{𝑠} ℂ = ℂ_{fld}$
38	37 27	eqeltri	$⊢ ℂ_{fld} ↾_{𝑠} ℂ \in CMetSp$
39	35 38	eqeltrdi	$⊢ K = ℂ \to ℂ_{fld} ↾_{𝑠} K \in CMetSp$
40	34 39	jaoi	$⊢ (K = ℝ \lor K = ℂ) \to ℂ_{fld} ↾_{𝑠} K \in CMetSp$
41	23 40	syl	$⊢ K \in \{ℝ, ℂ\} \to ℂ_{fld} ↾_{𝑠} K \in CMetSp$
42	22 41	impbid1	$⊢ W \in CPreHil \to (ℂ_{fld} ↾_{𝑠} K \in CMetSp \leftrightarrow K \in \{ℝ, ℂ\})$
43	13 42	bitrd	$⊢ W \in CPreHil \to (F \in CMetSp \leftrightarrow K \in \{ℝ, ℂ\})$
44	43	anbi2d	$⊢ W \in CPreHil \to ((W \in CMetSp \land F \in CMetSp) \leftrightarrow (W \in CMetSp \land K \in \{ℝ, ℂ\}))$
45	11 44	bitrd	$⊢ W \in CPreHil \to (W \in Ban \leftrightarrow (W \in CMetSp \land K \in \{ℝ, ℂ\}))$
46	45	pm5.32ri	$⊢ (W \in Ban \land W \in CPreHil) \leftrightarrow ((W \in CMetSp \land K \in \{ℝ, ℂ\}) \land W \in CPreHil)$
47	4 5 46	3bitr4ri	$⊢ (W \in Ban \land W \in CPreHil) \leftrightarrow (W \in CMetSp \land W \in CPreHil \land K \in \{ℝ, ℂ\})$
48	3 47	bitri	$⊢ W \in ℂHil \leftrightarrow (W \in CMetSp \land W \in CPreHil \land K \in \{ℝ, ℂ\})$

Metamath Proof Explorer

Theorem ishl2

Proof