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

Proof

Step	Hyp	Ref	Expression
1		2fveq3	|- ( A = if ( A e. CH , A , ~H ) -> ( _|_ ` ( _|_ ` A ) ) = ( _|_ ` ( _|_ ` if ( A e. CH , A , ~H ) ) ) )
2		id	|- ( A = if ( A e. CH , A , ~H ) -> A = if ( A e. CH , A , ~H ) )
3	1 2	eqeq12d	|- ( A = if ( A e. CH , A , ~H ) -> ( ( _|_ ` ( _|_ ` A ) ) = A <-> ( _|_ ` ( _|_ ` if ( A e. CH , A , ~H ) ) ) = if ( A e. CH , A , ~H ) ) )
4		ifchhv	|- if ( A e. CH , A , ~H ) e. CH
5	4	ococi	|- ( _|_ ` ( _|_ ` if ( A e. CH , A , ~H ) ) ) = if ( A e. CH , A , ~H )
6	3 5	dedth	|- ( A e. CH -> ( _|_ ` ( _|_ ` A ) ) = A )