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 )