# Metamath Proof Explorer

## Theorem ococi

Description: Complement of complement of a closed subspace of Hilbert space. Theorem 3.7(ii) of Beran p. 102. (Contributed by NM, 11-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis ococ.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
Assertion ococi ${⊢}\perp \left(\perp \left({A}\right)\right)={A}$

### Proof

Step Hyp Ref Expression
1 ococ.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 1 chshii ${⊢}{A}\in {\mathbf{S}}_{ℋ}$
3 shocsh ${⊢}{A}\in {\mathbf{S}}_{ℋ}\to \perp \left({A}\right)\in {\mathbf{S}}_{ℋ}$
4 2 3 ax-mp ${⊢}\perp \left({A}\right)\in {\mathbf{S}}_{ℋ}$
5 shocsh ${⊢}\perp \left({A}\right)\in {\mathbf{S}}_{ℋ}\to \perp \left(\perp \left({A}\right)\right)\in {\mathbf{S}}_{ℋ}$
6 4 5 ax-mp ${⊢}\perp \left(\perp \left({A}\right)\right)\in {\mathbf{S}}_{ℋ}$
7 shococss ${⊢}{A}\in {\mathbf{S}}_{ℋ}\to {A}\subseteq \perp \left(\perp \left({A}\right)\right)$
8 2 7 ax-mp ${⊢}{A}\subseteq \perp \left(\perp \left({A}\right)\right)$
9 incom ${⊢}\perp \left(\perp \left({A}\right)\right)\cap \perp \left({A}\right)=\perp \left({A}\right)\cap \perp \left(\perp \left({A}\right)\right)$
10 ocin ${⊢}\perp \left({A}\right)\in {\mathbf{S}}_{ℋ}\to \perp \left({A}\right)\cap \perp \left(\perp \left({A}\right)\right)={0}_{ℋ}$
11 4 10 ax-mp ${⊢}\perp \left({A}\right)\cap \perp \left(\perp \left({A}\right)\right)={0}_{ℋ}$
12 9 11 eqtri ${⊢}\perp \left(\perp \left({A}\right)\right)\cap \perp \left({A}\right)={0}_{ℋ}$
13 1 6 8 12 omlsii ${⊢}{A}=\perp \left(\perp \left({A}\right)\right)$
14 13 eqcomi ${⊢}\perp \left(\perp \left({A}\right)\right)={A}$