clsocv

Description: The orthogonal complement of the closure of a subset is the same as the orthogonal complement of the subset itself. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	clsocv.v	$⊢ V = {Base}_{W}$
	clsocv.o	$⊢ O = ocv (W)$
	clsocv.j	$⊢ J = TopOpen (W)$
Assertion	clsocv	$⊢ (W \in CPreHil \land S \subseteq V) \to O (cls (J) (S)) = O (S)$

Proof

Step	Hyp	Ref	Expression
1		clsocv.v	$⊢ V = {Base}_{W}$
2		clsocv.o	$⊢ O = ocv (W)$
3		clsocv.j	$⊢ J = TopOpen (W)$
4		cphngp	$⊢ W \in CPreHil \to W \in NrmGrp$
5		ngptps	$⊢ W \in NrmGrp \to W \in TopSp$
6	4 5	syl	$⊢ W \in CPreHil \to W \in TopSp$
7	6	adantr	$⊢ (W \in CPreHil \land S \subseteq V) \to W \in TopSp$
8	1 3	istps	$⊢ W \in TopSp \leftrightarrow J \in TopOn (V)$
9	7 8	sylib	$⊢ (W \in CPreHil \land S \subseteq V) \to J \in TopOn (V)$
10		topontop	$⊢ J \in TopOn (V) \to J \in Top$
11	9 10	syl	$⊢ (W \in CPreHil \land S \subseteq V) \to J \in Top$
12		simpr	$⊢ (W \in CPreHil \land S \subseteq V) \to S \subseteq V$
13		toponuni	$⊢ J \in TopOn (V) \to V = ⋃ J$
14	9 13	syl	$⊢ (W \in CPreHil \land S \subseteq V) \to V = ⋃ J$
15	12 14	sseqtrd	$⊢ (W \in CPreHil \land S \subseteq V) \to S \subseteq ⋃ J$
16		eqid	$⊢ ⋃ J = ⋃ J$
17	16	sscls	$⊢ (J \in Top \land S \subseteq ⋃ J) \to S \subseteq cls (J) (S)$
18	11 15 17	syl2anc	$⊢ (W \in CPreHil \land S \subseteq V) \to S \subseteq cls (J) (S)$
19	2	ocv2ss	$⊢ S \subseteq cls (J) (S) \to O (cls (J) (S)) \subseteq O (S)$
20	18 19	syl	$⊢ (W \in CPreHil \land S \subseteq V) \to O (cls (J) (S)) \subseteq O (S)$
21	16	clsss3	$⊢ (J \in Top \land S \subseteq ⋃ J) \to cls (J) (S) \subseteq ⋃ J$
22	11 15 21	syl2anc	$⊢ (W \in CPreHil \land S \subseteq V) \to cls (J) (S) \subseteq ⋃ J$
23	22 14	sseqtrrd	$⊢ (W \in CPreHil \land S \subseteq V) \to cls (J) (S) \subseteq V$
24	23	adantr	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to cls (J) (S) \subseteq V$
25	1 2	ocvss	$⊢ O (S) \subseteq V$
26	25	a1i	$⊢ (W \in CPreHil \land S \subseteq V) \to O (S) \subseteq V$
27	26	sselda	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to x \in V$
28		dfss2	$⊢ cls (J) (S) \subseteq V \leftrightarrow cls (J) (S) \cap V = cls (J) (S)$
29	24 28	sylib	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to cls (J) (S) \cap V = cls (J) (S)$
30	29	ineq1d	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to (cls (J) (S) \cap V) \cap \{y \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} = cls (J) (S) \cap \{y \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\}$
31		dfrab3	$⊢ \{y \in V \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} = V \cap \{y \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\}$
32	31	ineq2i	$⊢ cls (J) (S) \cap \{y \in V \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} = cls (J) (S) \cap (V \cap \{y \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\})$
33		inass	$⊢ (cls (J) (S) \cap V) \cap \{y \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} = cls (J) (S) \cap (V \cap \{y \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\})$
34	32 33	eqtr4i	$⊢ cls (J) (S) \cap \{y \in V \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} = (cls (J) (S) \cap V) \cap \{y \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\}$
35		dfrab3	$⊢ \{y \in cls (J) (S) \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} = cls (J) (S) \cap \{y \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\}$
36	30 34 35	3eqtr4g	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to cls (J) (S) \cap \{y \in V \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} = \{y \in cls (J) (S) \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\}$
37	16	clscld	$⊢ (J \in Top \land S \subseteq ⋃ J) \to cls (J) (S) \in Clsd (J)$
38	11 15 37	syl2anc	$⊢ (W \in CPreHil \land S \subseteq V) \to cls (J) (S) \in Clsd (J)$
39	38	adantr	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to cls (J) (S) \in Clsd (J)$
40		fvex	$⊢ 0_{Scalar (W)} \in V$
41		eqid	$⊢ (y \in V ⟼ x \cdot_{𝑖} (W) y) = (y \in V ⟼ x \cdot_{𝑖} (W) y)$
42	41	mptiniseg	$⊢ 0_{Scalar (W)} \in V \to {(y \in V ⟼ x \cdot_{𝑖} (W) y)}^{-1} [\{0_{Scalar (W)}\}] = \{y \in V \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\}$
43	40 42	ax-mp	$⊢ {(y \in V ⟼ x \cdot_{𝑖} (W) y)}^{-1} [\{0_{Scalar (W)}\}] = \{y \in V \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\}$
44		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
45		eqid	$⊢ \cdot_{𝑖} (W) = \cdot_{𝑖} (W)$
46		simpll	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to W \in CPreHil$
47	9	adantr	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to J \in TopOn (V)$
48	47 47 27	cnmptc	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to (y \in V ⟼ x) \in (J Cn J)$
49	47	cnmptid	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to (y \in V ⟼ y) \in (J Cn J)$
50	3 44 45 46 47 48 49	cnmpt1ip	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to (y \in V ⟼ x \cdot_{𝑖} (W) y) \in (J Cn TopOpen (ℂ_{fld}))$
51	44	cnfldhaus	$⊢ TopOpen (ℂ_{fld}) \in Haus$
52		cphclm	$⊢ W \in CPreHil \to W \in CMod$
53		eqid	$⊢ Scalar (W) = Scalar (W)$
54	53	clm0	$⊢ W \in CMod \to 0 = 0_{Scalar (W)}$
55	52 54	syl	$⊢ W \in CPreHil \to 0 = 0_{Scalar (W)}$
56	55	ad2antrr	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to 0 = 0_{Scalar (W)}$
57		0cn	$⊢ 0 \in ℂ$
58	56 57	eqeltrrdi	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to 0_{Scalar (W)} \in ℂ$
59		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
60	59	sncld	$⊢ (TopOpen (ℂ_{fld}) \in Haus \land 0_{Scalar (W)} \in ℂ) \to \{0_{Scalar (W)}\} \in Clsd (TopOpen (ℂ_{fld}))$
61	51 58 60	sylancr	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to \{0_{Scalar (W)}\} \in Clsd (TopOpen (ℂ_{fld}))$
62		cnclima	$⊢ ((y \in V ⟼ x \cdot_{𝑖} (W) y) \in (J Cn TopOpen (ℂ_{fld})) \land \{0_{Scalar (W)}\} \in Clsd (TopOpen (ℂ_{fld}))) \to {(y \in V ⟼ x \cdot_{𝑖} (W) y)}^{-1} [\{0_{Scalar (W)}\}] \in Clsd (J)$
63	50 61 62	syl2anc	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to {(y \in V ⟼ x \cdot_{𝑖} (W) y)}^{-1} [\{0_{Scalar (W)}\}] \in Clsd (J)$
64	43 63	eqeltrrid	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to \{y \in V \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} \in Clsd (J)$
65		incld	$⊢ (cls (J) (S) \in Clsd (J) \land \{y \in V \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} \in Clsd (J)) \to cls (J) (S) \cap \{y \in V \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} \in Clsd (J)$
66	39 64 65	syl2anc	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to cls (J) (S) \cap \{y \in V \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} \in Clsd (J)$
67	36 66	eqeltrrd	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to \{y \in cls (J) (S) \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} \in Clsd (J)$
68	18	adantr	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to S \subseteq cls (J) (S)$
69		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
70	1 45 53 69 2	ocvi	$⊢ (x \in O (S) \land y \in S) \to x \cdot_{𝑖} (W) y = 0_{Scalar (W)}$
71	70	ralrimiva	$⊢ x \in O (S) \to \forall y \in S x \cdot_{𝑖} (W) y = 0_{Scalar (W)}$
72	71	adantl	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to \forall y \in S x \cdot_{𝑖} (W) y = 0_{Scalar (W)}$
73		ssrab	$⊢ S \subseteq \{y \in cls (J) (S) \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} \leftrightarrow (S \subseteq cls (J) (S) \land \forall y \in S x \cdot_{𝑖} (W) y = 0_{Scalar (W)})$
74	68 72 73	sylanbrc	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to S \subseteq \{y \in cls (J) (S) \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\}$
75	16	clsss2	$⊢ (\{y \in cls (J) (S) \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} \in Clsd (J) \land S \subseteq \{y \in cls (J) (S) \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\}) \to cls (J) (S) \subseteq \{y \in cls (J) (S) \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\}$
76	67 74 75	syl2anc	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to cls (J) (S) \subseteq \{y \in cls (J) (S) \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\}$
77		ssrab2	$⊢ \{y \in cls (J) (S) \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} \subseteq cls (J) (S)$
78	77	a1i	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to \{y \in cls (J) (S) \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} \subseteq cls (J) (S)$
79	76 78	eqssd	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to cls (J) (S) = \{y \in cls (J) (S) \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\}$
80		rabid2	$⊢ cls (J) (S) = \{y \in cls (J) (S) \| x \cdot_{𝑖} (W) y = 0_{Scalar (W)}\} \leftrightarrow \forall y \in cls (J) (S) x \cdot_{𝑖} (W) y = 0_{Scalar (W)}$
81	79 80	sylib	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to \forall y \in cls (J) (S) x \cdot_{𝑖} (W) y = 0_{Scalar (W)}$
82	1 45 53 69 2	elocv	$⊢ x \in O (cls (J) (S)) \leftrightarrow (cls (J) (S) \subseteq V \land x \in V \land \forall y \in cls (J) (S) x \cdot_{𝑖} (W) y = 0_{Scalar (W)})$
83	24 27 81 82	syl3anbrc	$⊢ ((W \in CPreHil \land S \subseteq V) \land x \in O (S)) \to x \in O (cls (J) (S))$
84	20 83	eqelssd	$⊢ (W \in CPreHil \land S \subseteq V) \to O (cls (J) (S)) = O (S)$

Metamath Proof Explorer

Theorem clsocv

Proof