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

Metamath Proof Explorer

Theorem chjo

Description: The join of a closed subspace and its orthocomplement is all of Hilbert space. (Contributed by NM, 31-Oct-2005) (New usage is discouraged.)

Ref Expression
Assertion chjo 
|- ( A e. CH -> ( A vH ( _|_ ` A ) ) = ~H )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A = if ( A e. CH , A , ~H ) -> A = if ( A e. CH , A , ~H ) )
2 fveq2 
 |-  ( A = if ( A e. CH , A , ~H ) -> ( _|_ ` A ) = ( _|_ ` if ( A e. CH , A , ~H ) ) )
3 1 2 oveq12d 
 |-  ( A = if ( A e. CH , A , ~H ) -> ( A vH ( _|_ ` A ) ) = ( if ( A e. CH , A , ~H ) vH ( _|_ ` if ( A e. CH , A , ~H ) ) ) )
4 3 eqeq1d 
 |-  ( A = if ( A e. CH , A , ~H ) -> ( ( A vH ( _|_ ` A ) ) = ~H <-> ( if ( A e. CH , A , ~H ) vH ( _|_ ` if ( A e. CH , A , ~H ) ) ) = ~H ) )
5 ifchhv 
 |-  if ( A e. CH , A , ~H ) e. CH
6 5 chjoi 
 |-  ( if ( A e. CH , A , ~H ) vH ( _|_ ` if ( A e. CH , A , ~H ) ) ) = ~H
7 4 6 dedth 
 |-  ( A e. CH -> ( A vH ( _|_ ` A ) ) = ~H )