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 e. CH
Assertion	ococi	|- ( _|_ ` ( _|_ ` A ) ) = A

Proof

Step	Hyp	Ref	Expression
1		ococ.1	|- A e. CH
2	1	chshii	|- A e. SH
3		shocsh	|- ( A e. SH -> ( _|_ ` A ) e. SH )
4	2 3	ax-mp	|- ( _|_ ` A ) e. SH
5		shocsh	|- ( ( _|_ ` A ) e. SH -> ( _|_ ` ( _|_ ` A ) ) e. SH )
6	4 5	ax-mp	|- ( _|_ ` ( _|_ ` A ) ) e. SH
7		shococss	|- ( A e. SH -> A C_ ( _|_ ` ( _|_ ` A ) ) )
8	2 7	ax-mp	|- A C_ ( _|_ ` ( _|_ ` A ) )
9		incom	|- ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` A ) ) = ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` A ) ) )
10		ocin	|- ( ( _|_ ` A ) e. SH -> ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` A ) ) ) = 0H )
11	4 10	ax-mp	|- ( ( _|_ ` A ) i^i ( _|_ ` ( _|_ ` A ) ) ) = 0H
12	9 11	eqtri	|- ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` A ) ) = 0H
13	1 6 8 12	omlsii	|- A = ( _|_ ` ( _|_ ` A ) )
14	13	eqcomi	|- ( _|_ ` ( _|_ ` A ) ) = A