cssmre

Description: The closed subspaces of a pre-Hilbert space are a Moore system. Unlike many of our other examples of closure systems, this one isnot usually an algebraic closure system df-acs : consider the Hilbert space of sequences NN --> RR with convergent sum; the subspace of all sequences with finite support is the classic example of a non-closed subspace, but for every finite set of sequences of finite support, there is a finite-dimensional (and hence closed) subspace containing all of the sequences, so if closed subspaces were an algebraic closure system this would violate acsfiel . (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	cssmre.v	$⊢ V = {Base}_{W}$
	cssmre.c	$⊢ C = ClSubSp (W)$
Assertion	cssmre	$⊢ W \in PreHil \to C \in Moore (V)$

Proof

Step	Hyp	Ref	Expression
1		cssmre.v	$⊢ V = {Base}_{W}$
2		cssmre.c	$⊢ C = ClSubSp (W)$
3	1 2	cssss	$⊢ x \in C \to x \subseteq V$
4		velpw	$⊢ x \in 𝒫 V \leftrightarrow x \subseteq V$
5	3 4	sylibr	$⊢ x \in C \to x \in 𝒫 V$
6	5	a1i	$⊢ W \in PreHil \to (x \in C \to x \in 𝒫 V)$
7	6	ssrdv	$⊢ W \in PreHil \to C \subseteq 𝒫 V$
8	1 2	css1	$⊢ W \in PreHil \to V \in C$
9		intss1	$⊢ z \in x \to ⋂ x \subseteq z$
10		eqid	$⊢ ocv (W) = ocv (W)$
11	10	ocv2ss	$⊢ ⋂ x \subseteq z \to ocv (W) (z) \subseteq ocv (W) (⋂ x)$
12	10	ocv2ss	$⊢ ocv (W) (z) \subseteq ocv (W) (⋂ x) \to ocv (W) (ocv (W) (⋂ x)) \subseteq ocv (W) (ocv (W) (z))$
13	9 11 12	3syl	$⊢ z \in x \to ocv (W) (ocv (W) (⋂ x)) \subseteq ocv (W) (ocv (W) (z))$
14	13	ad2antll	$⊢ ((W \in PreHil \land x \subseteq C \land x \neq \emptyset) \land (y \in ocv (W) (ocv (W) (⋂ x)) \land z \in x)) \to ocv (W) (ocv (W) (⋂ x)) \subseteq ocv (W) (ocv (W) (z))$
15		simprl	$⊢ ((W \in PreHil \land x \subseteq C \land x \neq \emptyset) \land (y \in ocv (W) (ocv (W) (⋂ x)) \land z \in x)) \to y \in ocv (W) (ocv (W) (⋂ x))$
16	14 15	sseldd	$⊢ ((W \in PreHil \land x \subseteq C \land x \neq \emptyset) \land (y \in ocv (W) (ocv (W) (⋂ x)) \land z \in x)) \to y \in ocv (W) (ocv (W) (z))$
17		simpl2	$⊢ ((W \in PreHil \land x \subseteq C \land x \neq \emptyset) \land (y \in ocv (W) (ocv (W) (⋂ x)) \land z \in x)) \to x \subseteq C$
18		simprr	$⊢ ((W \in PreHil \land x \subseteq C \land x \neq \emptyset) \land (y \in ocv (W) (ocv (W) (⋂ x)) \land z \in x)) \to z \in x$
19	17 18	sseldd	$⊢ ((W \in PreHil \land x \subseteq C \land x \neq \emptyset) \land (y \in ocv (W) (ocv (W) (⋂ x)) \land z \in x)) \to z \in C$
20	10 2	cssi	$⊢ z \in C \to z = ocv (W) (ocv (W) (z))$
21	19 20	syl	$⊢ ((W \in PreHil \land x \subseteq C \land x \neq \emptyset) \land (y \in ocv (W) (ocv (W) (⋂ x)) \land z \in x)) \to z = ocv (W) (ocv (W) (z))$
22	16 21	eleqtrrd	$⊢ ((W \in PreHil \land x \subseteq C \land x \neq \emptyset) \land (y \in ocv (W) (ocv (W) (⋂ x)) \land z \in x)) \to y \in z$
23	22	expr	$⊢ ((W \in PreHil \land x \subseteq C \land x \neq \emptyset) \land y \in ocv (W) (ocv (W) (⋂ x))) \to (z \in x \to y \in z)$
24	23	alrimiv	$⊢ ((W \in PreHil \land x \subseteq C \land x \neq \emptyset) \land y \in ocv (W) (ocv (W) (⋂ x))) \to \forall z (z \in x \to y \in z)$
25		vex	$⊢ y \in V$
26	25	elint	$⊢ y \in ⋂ x \leftrightarrow \forall z (z \in x \to y \in z)$
27	24 26	sylibr	$⊢ ((W \in PreHil \land x \subseteq C \land x \neq \emptyset) \land y \in ocv (W) (ocv (W) (⋂ x))) \to y \in ⋂ x$
28	27	ex	$⊢ (W \in PreHil \land x \subseteq C \land x \neq \emptyset) \to (y \in ocv (W) (ocv (W) (⋂ x)) \to y \in ⋂ x)$
29	28	ssrdv	$⊢ (W \in PreHil \land x \subseteq C \land x \neq \emptyset) \to ocv (W) (ocv (W) (⋂ x)) \subseteq ⋂ x$
30		simp1	$⊢ (W \in PreHil \land x \subseteq C \land x \neq \emptyset) \to W \in PreHil$
31		intssuni	$⊢ x \neq \emptyset \to ⋂ x \subseteq ⋃ x$
32	31	3ad2ant3	$⊢ (W \in PreHil \land x \subseteq C \land x \neq \emptyset) \to ⋂ x \subseteq ⋃ x$
33		simp2	$⊢ (W \in PreHil \land x \subseteq C \land x \neq \emptyset) \to x \subseteq C$
34	7	3ad2ant1	$⊢ (W \in PreHil \land x \subseteq C \land x \neq \emptyset) \to C \subseteq 𝒫 V$
35	33 34	sstrd	$⊢ (W \in PreHil \land x \subseteq C \land x \neq \emptyset) \to x \subseteq 𝒫 V$
36		sspwuni	$⊢ x \subseteq 𝒫 V \leftrightarrow ⋃ x \subseteq V$
37	35 36	sylib	$⊢ (W \in PreHil \land x \subseteq C \land x \neq \emptyset) \to ⋃ x \subseteq V$
38	32 37	sstrd	$⊢ (W \in PreHil \land x \subseteq C \land x \neq \emptyset) \to ⋂ x \subseteq V$
39	1 2 10	iscss2	$⊢ (W \in PreHil \land ⋂ x \subseteq V) \to (⋂ x \in C \leftrightarrow ocv (W) (ocv (W) (⋂ x)) \subseteq ⋂ x)$
40	30 38 39	syl2anc	$⊢ (W \in PreHil \land x \subseteq C \land x \neq \emptyset) \to (⋂ x \in C \leftrightarrow ocv (W) (ocv (W) (⋂ x)) \subseteq ⋂ x)$
41	29 40	mpbird	$⊢ (W \in PreHil \land x \subseteq C \land x \neq \emptyset) \to ⋂ x \in C$
42	7 8 41	ismred	$⊢ W \in PreHil \to C \in Moore (V)$

Metamath Proof Explorer

Theorem cssmre

Proof