# Metamath Proof Explorer

## Theorem ococ

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
Assertion ococ ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \perp \left(\perp \left({A}\right)\right)={A}$

### Proof

Step Hyp Ref Expression
1 2fveq3 ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to \perp \left(\perp \left({A}\right)\right)=\perp \left(\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\right)\right)$
2 id ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to {A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)$
3 1 2 eqeq12d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\to \left(\perp \left(\perp \left({A}\right)\right)={A}↔\perp \left(\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\right)\right)=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\right)$
4 ifchhv ${⊢}if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\in {\mathbf{C}}_{ℋ}$
5 4 ococi ${⊢}\perp \left(\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)\right)\right)=if\left({A}\in {\mathbf{C}}_{ℋ},{A},ℋ\right)$
6 3 5 dedth ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \perp \left(\perp \left({A}\right)\right)={A}$