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}}_{\mathscr{H}}\to \perp \left(\perp \left(A\right)\right)=A$$

Proof

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