Theorem cssi

Description: Property of a closed subspace (of a pre-Hilbert space). (Contributed 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	cssi	$$⊢S\in C\to S=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(S\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		elfvdm	$$⊢S\in \mathrm{ClSubSp}\left(W\right)\to W\in \mathrm{dom}\mathrm{ClSubSp}$$
4	3 2	eleq2s	$$⊢S\in C\to W\in \mathrm{dom}\mathrm{ClSubSp}$$
5	1 2	iscss	$$⊢W\in \mathrm{dom}\mathrm{ClSubSp}\to \left(S\in C\leftrightarrow S=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(S\right)\right)\right)$$
6	4 5	syl	$$⊢S\in C\to \left(S\in C\leftrightarrow S=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(S\right)\right)\right)$$
7	6	ibi	$$⊢S\in C\to S=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(S\right)\right)$$