lsmcss

Description: A subset of a pre-Hilbert space whose double orthocomplement has a projection decomposition is a closed subspace. This is the core of the proof that a topologically closed subspace is algebraically closed in a Hilbert space. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	lsmcss.c	$⊢ C = ClSubSp (W)$
	lsmcss.j	$⊢ V = {Base}_{W}$
	lsmcss.o	$⊢ \underset{˙}{⊥} = ocv (W)$
	lsmcss.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	lsmcss.1	$⊢ φ \to W \in PreHil$
	lsmcss.2	$⊢ φ \to S \subseteq V$
	lsmcss.3	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq S \underset{˙}{\oplus} \underset{˙}{⊥} (S)$
Assertion	lsmcss	$⊢ φ \to S \in C$

Proof

Step	Hyp	Ref	Expression
1		lsmcss.c	$⊢ C = ClSubSp (W)$
2		lsmcss.j	$⊢ V = {Base}_{W}$
3		lsmcss.o	$⊢ \underset{˙}{⊥} = ocv (W)$
4		lsmcss.p	$⊢ \underset{˙}{\oplus} = LSSum (W)$
5		lsmcss.1	$⊢ φ \to W \in PreHil$
6		lsmcss.2	$⊢ φ \to S \subseteq V$
7		lsmcss.3	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq S \underset{˙}{\oplus} \underset{˙}{⊥} (S)$
8	7	sseld	$⊢ φ \to (x \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to x \in (S \underset{˙}{\oplus} \underset{˙}{⊥} (S)))$
9		phllmod	$⊢ W \in PreHil \to W \in LMod$
10	5 9	syl	$⊢ φ \to W \in LMod$
11	2 3	ocvss	$⊢ \underset{˙}{⊥} (S) \subseteq V$
12	11	a1i	$⊢ φ \to \underset{˙}{⊥} (S) \subseteq V$
13		eqid	$⊢ +_{W} = +_{W}$
14	2 13 4	lsmelvalx	$⊢ (W \in LMod \land S \subseteq V \land \underset{˙}{⊥} (S) \subseteq V) \to (x \in (S \underset{˙}{\oplus} \underset{˙}{⊥} (S)) \leftrightarrow \exists y \in S \exists z \in \underset{˙}{⊥} (S) x = y +_{W} z)$
15	10 6 12 14	syl3anc	$⊢ φ \to (x \in (S \underset{˙}{\oplus} \underset{˙}{⊥} (S)) \leftrightarrow \exists y \in S \exists z \in \underset{˙}{⊥} (S) x = y +_{W} z)$
16	8 15	sylibd	$⊢ φ \to (x \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to \exists y \in S \exists z \in \underset{˙}{⊥} (S) x = y +_{W} z)$
17	5	ad2antrr	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to W \in PreHil$
18	6	ad2antrr	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to S \subseteq V$
19		simplrl	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to y \in S$
20	18 19	sseldd	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to y \in V$
21		simplrr	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to z \in \underset{˙}{⊥} (S)$
22	11 21	sseldi	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to z \in V$
23		eqid	$⊢ Scalar (W) = Scalar (W)$
24		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
25		eqid	$⊢ +_{Scalar (W)} = +_{Scalar (W)}$
26	23 24 2 13 25	ipdir	$⊢ (W \in PreHil \land (y \in V \land z \in V \land z \in V)) \to (y +_{W} z) \cdot_{𝑖} (W) z = (y \cdot_{𝑖} (W) z) +_{Scalar (W)} (z \cdot_{𝑖} (W) z)$
27	17 20 22 22 26	syl13anc	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to (y +_{W} z) \cdot_{𝑖} (W) z = (y \cdot_{𝑖} (W) z) +_{Scalar (W)} (z \cdot_{𝑖} (W) z)$
28		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
29	2 24 23 28 3	ocvi	$⊢ (z \in \underset{˙}{⊥} (S) \land y \in S) \to z \cdot_{𝑖} (W) y = 0_{Scalar (W)}$
30	21 19 29	syl2anc	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to z \cdot_{𝑖} (W) y = 0_{Scalar (W)}$
31	23 24 2 28	iporthcom	$⊢ (W \in PreHil \land z \in V \land y \in V) \to (z \cdot_{𝑖} (W) y = 0_{Scalar (W)} \leftrightarrow y \cdot_{𝑖} (W) z = 0_{Scalar (W)})$
32	17 22 20 31	syl3anc	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to (z \cdot_{𝑖} (W) y = 0_{Scalar (W)} \leftrightarrow y \cdot_{𝑖} (W) z = 0_{Scalar (W)})$
33	30 32	mpbid	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to y \cdot_{𝑖} (W) z = 0_{Scalar (W)}$
34	33	oveq1d	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to (y \cdot_{𝑖} (W) z) +_{Scalar (W)} (z \cdot_{𝑖} (W) z) = 0_{Scalar (W)} +_{Scalar (W)} (z \cdot_{𝑖} (W) z)$
35	17 9	syl	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to W \in LMod$
36	23	lmodfgrp	$⊢ W \in LMod \to Scalar (W) \in Grp$
37	35 36	syl	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to Scalar (W) \in Grp$
38		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
39	23 24 2 38	ipcl	$⊢ (W \in PreHil \land z \in V \land z \in V) \to z \cdot_{𝑖} (W) z \in {Base}_{Scalar (W)}$
40	17 22 22 39	syl3anc	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to z \cdot_{𝑖} (W) z \in {Base}_{Scalar (W)}$
41	38 25 28	grplid	$⊢ (Scalar (W) \in Grp \land z \cdot_{𝑖} (W) z \in {Base}_{Scalar (W)}) \to 0_{Scalar (W)} +_{Scalar (W)} (z \cdot_{𝑖} (W) z) = z \cdot_{𝑖} (W) z$
42	37 40 41	syl2anc	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to 0_{Scalar (W)} +_{Scalar (W)} (z \cdot_{𝑖} (W) z) = z \cdot_{𝑖} (W) z$
43	27 34 42	3eqtrd	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to (y +_{W} z) \cdot_{𝑖} (W) z = z \cdot_{𝑖} (W) z$
44		simpr	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))$
45	2 24 23 28 3	ocvi	$⊢ (y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \land z \in \underset{˙}{⊥} (S)) \to (y +_{W} z) \cdot_{𝑖} (W) z = 0_{Scalar (W)}$
46	44 21 45	syl2anc	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to (y +_{W} z) \cdot_{𝑖} (W) z = 0_{Scalar (W)}$
47	43 46	eqtr3d	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to z \cdot_{𝑖} (W) z = 0_{Scalar (W)}$
48		eqid	$⊢ 0_{W} = 0_{W}$
49	23 24 2 28 48	ipeq0	$⊢ (W \in PreHil \land z \in V) \to (z \cdot_{𝑖} (W) z = 0_{Scalar (W)} \leftrightarrow z = 0_{W})$
50	17 22 49	syl2anc	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to (z \cdot_{𝑖} (W) z = 0_{Scalar (W)} \leftrightarrow z = 0_{W})$
51	47 50	mpbid	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to z = 0_{W}$
52	51	oveq2d	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to y +_{W} z = y +_{W} 0_{W}$
53		lmodgrp	$⊢ W \in LMod \to W \in Grp$
54	10 53	syl	$⊢ φ \to W \in Grp$
55	54	ad2antrr	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to W \in Grp$
56	2 13 48	grprid	$⊢ (W \in Grp \land y \in V) \to y +_{W} 0_{W} = y$
57	55 20 56	syl2anc	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to y +_{W} 0_{W} = y$
58	52 57	eqtrd	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to y +_{W} z = y$
59	58 19	eqeltrd	$⊢ ((φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \land y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S))) \to y +_{W} z \in S$
60	59	ex	$⊢ (φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \to (y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to y +_{W} z \in S)$
61		eleq1	$⊢ x = y +_{W} z \to (x \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \leftrightarrow y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)))$
62		eleq1	$⊢ x = y +_{W} z \to (x \in S \leftrightarrow y +_{W} z \in S)$
63	61 62	imbi12d	$⊢ x = y +_{W} z \to ((x \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to x \in S) \leftrightarrow (y +_{W} z \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to y +_{W} z \in S))$
64	60 63	syl5ibrcom	$⊢ (φ \land (y \in S \land z \in \underset{˙}{⊥} (S))) \to (x = y +_{W} z \to (x \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to x \in S))$
65	64	rexlimdvva	$⊢ φ \to (\exists y \in S \exists z \in \underset{˙}{⊥} (S) x = y +_{W} z \to (x \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to x \in S))$
66	16 65	syld	$⊢ φ \to (x \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to (x \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to x \in S))$
67	66	pm2.43d	$⊢ φ \to (x \in \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \to x \in S)$
68	67	ssrdv	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq S$
69	2 1 3	iscss2	$⊢ (W \in PreHil \land S \subseteq V) \to (S \in C \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq S)$
70	5 6 69	syl2anc	$⊢ φ \to (S \in C \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (S)) \subseteq S)$
71	68 70	mpbird	$⊢ φ \to S \in C$

Metamath Proof Explorer

Theorem lsmcss

Proof