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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	cssmre.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
Assertion	cssmre	⊢ ( 𝑊 ∈ PreHil → 𝐶 ∈ ( Moore ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		cssmre.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		cssmre.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
3	1 2	cssss	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ⊆ 𝑉 )
4		velpw	⊢ ( 𝑥 ∈ 𝒫 𝑉 ↔ 𝑥 ⊆ 𝑉 )
5	3 4	sylibr	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝒫 𝑉 )
6	5	a1i	⊢ ( 𝑊 ∈ PreHil → ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝒫 𝑉 ) )
7	6	ssrdv	⊢ ( 𝑊 ∈ PreHil → 𝐶 ⊆ 𝒫 𝑉 )
8	1 2	css1	⊢ ( 𝑊 ∈ PreHil → 𝑉 ∈ 𝐶 )
9		intss1	⊢ ( 𝑧 ∈ 𝑥 → ∩ 𝑥 ⊆ 𝑧 )
10		eqid	⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
11	10	ocv2ss	⊢ ( ∩ 𝑥 ⊆ 𝑧 → ( ( ocv ‘ 𝑊 ) ‘ 𝑧 ) ⊆ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) )
12	10	ocv2ss	⊢ ( ( ( ocv ‘ 𝑊 ) ‘ 𝑧 ) ⊆ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ⊆ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑧 ) ) )
13	9 11 12	3syl	⊢ ( 𝑧 ∈ 𝑥 → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ⊆ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑧 ) ) )
14	13	ad2antll	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) ∧ ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ∧ 𝑧 ∈ 𝑥 ) ) → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ⊆ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑧 ) ) )
15		simprl	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) ∧ ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ∧ 𝑧 ∈ 𝑥 ) ) → 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) )
16	14 15	sseldd	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) ∧ ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ∧ 𝑧 ∈ 𝑥 ) ) → 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑧 ) ) )
17		simpl2	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) ∧ ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ∧ 𝑧 ∈ 𝑥 ) ) → 𝑥 ⊆ 𝐶 )
18		simprr	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) ∧ ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ∧ 𝑧 ∈ 𝑥 ) ) → 𝑧 ∈ 𝑥 )
19	17 18	sseldd	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) ∧ ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ∧ 𝑧 ∈ 𝑥 ) ) → 𝑧 ∈ 𝐶 )
20	10 2	cssi	⊢ ( 𝑧 ∈ 𝐶 → 𝑧 = ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑧 ) ) )
21	19 20	syl	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) ∧ ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ∧ 𝑧 ∈ 𝑥 ) ) → 𝑧 = ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ 𝑧 ) ) )
22	16 21	eleqtrrd	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) ∧ ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ∧ 𝑧 ∈ 𝑥 ) ) → 𝑦 ∈ 𝑧 )
23	22	expr	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ) → ( 𝑧 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) )
24	23	alrimiv	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ) → ∀ 𝑧 ( 𝑧 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) )
25		vex	⊢ 𝑦 ∈ V
26	25	elint	⊢ ( 𝑦 ∈ ∩ 𝑥 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) )
27	24 26	sylibr	⊢ ( ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) ∧ 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ) → 𝑦 ∈ ∩ 𝑥 )
28	27	ex	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → ( 𝑦 ∈ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) → 𝑦 ∈ ∩ 𝑥 ) )
29	28	ssrdv	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ⊆ ∩ 𝑥 )
30		simp1	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → 𝑊 ∈ PreHil )
31		intssuni	⊢ ( 𝑥 ≠ ∅ → ∩ 𝑥 ⊆ ∪ 𝑥 )
32	31	3ad2ant3	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → ∩ 𝑥 ⊆ ∪ 𝑥 )
33		simp2	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → 𝑥 ⊆ 𝐶 )
34	7	3ad2ant1	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → 𝐶 ⊆ 𝒫 𝑉 )
35	33 34	sstrd	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → 𝑥 ⊆ 𝒫 𝑉 )
36		sspwuni	⊢ ( 𝑥 ⊆ 𝒫 𝑉 ↔ ∪ 𝑥 ⊆ 𝑉 )
37	35 36	sylib	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → ∪ 𝑥 ⊆ 𝑉 )
38	32 37	sstrd	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → ∩ 𝑥 ⊆ 𝑉 )
39	1 2 10	iscss2	⊢ ( ( 𝑊 ∈ PreHil ∧ ∩ 𝑥 ⊆ 𝑉 ) → ( ∩ 𝑥 ∈ 𝐶 ↔ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ⊆ ∩ 𝑥 ) )
40	30 38 39	syl2anc	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → ( ∩ 𝑥 ∈ 𝐶 ↔ ( ( ocv ‘ 𝑊 ) ‘ ( ( ocv ‘ 𝑊 ) ‘ ∩ 𝑥 ) ) ⊆ ∩ 𝑥 ) )
41	29 40	mpbird	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → ∩ 𝑥 ∈ 𝐶 )
42	7 8 41	ismred	⊢ ( 𝑊 ∈ PreHil → 𝐶 ∈ ( Moore ‘ 𝑉 ) )

Metamath Proof Explorer

Theorem cssmre

Proof