Theorem cssval

Description: The set of closed subspaces of a pre-Hilbert space. (Contributed by NM, 7-Oct-2011) (Revised by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	cssval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
	cssval.c	$$⊢C=\mathrm{ClSubSp}\left(W\right)$$
Assertion	cssval	$$⊢W\in X\to C=\left\{s|s=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cssval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
2		cssval.c	$$⊢C=\mathrm{ClSubSp}\left(W\right)$$
3		elex	$$⊢W\in X\to W\in \mathrm{V}$$
4		fveq2	$$⊢w=W\to \mathrm{ocv}\left(w\right)=\mathrm{ocv}\left(W\right)$$
5	4 1	eqtr4di	$$⊢w=W\to \mathrm{ocv}\left(w\right)=\underset{\dot{}}{\perp }$$
6	5	fveq1d	$$⊢w=W\to \mathrm{ocv}\left(w\right)\left(s\right)=\underset{\dot{}}{\perp }\left(s\right)$$
7	5 6	fveq12d	$$⊢w=W\to \mathrm{ocv}\left(w\right)\left(\mathrm{ocv}\left(w\right)\left(s\right)\right)=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)$$
8	7	eqeq2d	$$⊢w=W\to \left(s=\mathrm{ocv}\left(w\right)\left(\mathrm{ocv}\left(w\right)\left(s\right)\right)\leftrightarrow s=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\right)$$
9	8	abbidv	$$⊢w=W\to \left\{s|s=\mathrm{ocv}\left(w\right)\left(\mathrm{ocv}\left(w\right)\left(s\right)\right)\right\}=\left\{s|s=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\right\}$$
10		df-css	$$⊢\mathrm{ClSubSp}=\left(w\in \mathrm{V}⟼\left\{s|s=\mathrm{ocv}\left(w\right)\left(\mathrm{ocv}\left(w\right)\left(s\right)\right)\right\}\right)$$
11		fvex	$$⊢{\mathrm{Base}}_W\in \mathrm{V}$$
12	11	pwex	$$⊢𝒫{\mathrm{Base}}_W\in \mathrm{V}$$
13		id	$$⊢s=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\to s=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)$$
14		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
15	14 1	ocvss	$$⊢\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\subseteq {\mathrm{Base}}_W$$
16		fvex	$$⊢\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\in \mathrm{V}$$
17	16	elpw	$$⊢\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\in 𝒫{\mathrm{Base}}_W\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\subseteq {\mathrm{Base}}_W$$
18	15 17	mpbir	$$⊢\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\in 𝒫{\mathrm{Base}}_W$$
19	13 18	eqeltrdi	$$⊢s=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\to s\in 𝒫{\mathrm{Base}}_W$$
20	19	abssi	$$⊢\left\{s|s=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\right\}\subseteq 𝒫{\mathrm{Base}}_W$$
21	12 20	ssexi	$$⊢\left\{s|s=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\right\}\in \mathrm{V}$$
22	9 10 21	fvmpt	$$⊢W\in \mathrm{V}\to \mathrm{ClSubSp}\left(W\right)=\left\{s|s=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\right\}$$
23	2 22	syl5eq	$$⊢W\in \mathrm{V}\to C=\left\{s|s=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\right\}$$
24	3 23	syl	$$⊢W\in X\to C=\left\{s|s=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(s\right)\right)\right\}$$