This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 )