Theorem pjoc1

Description: Projection of a vector in the orthocomplement of the projection subspace. (Contributed by NM, 6-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	pjoc1	|- ( ( H e. CH /\ A e. ~H ) -> ( A e. H <-> ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h ) )

Proof

Step	Hyp	Ref	Expression
1		eleq2	|- ( H = if ( H e. CH , H , ~H ) -> ( A e. H <-> A e. if ( H e. CH , H , ~H ) ) )
2		2fveq3	|- ( H = if ( H e. CH , H , ~H ) -> ( projh ` ( _|_ ` H ) ) = ( projh ` ( _|_ ` if ( H e. CH , H , ~H ) ) ) )
3	2	fveq1d	|- ( H = if ( H e. CH , H , ~H ) -> ( ( projh ` ( _|_ ` H ) ) ` A ) = ( ( projh ` ( _|_ ` if ( H e. CH , H , ~H ) ) ) ` A ) )
4	3	eqeq1d	|- ( H = if ( H e. CH , H , ~H ) -> ( ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h <-> ( ( projh ` ( _|_ ` if ( H e. CH , H , ~H ) ) ) ` A ) = 0h ) )
5	1 4	bibi12d	|- ( H = if ( H e. CH , H , ~H ) -> ( ( A e. H <-> ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h ) <-> ( A e. if ( H e. CH , H , ~H ) <-> ( ( projh ` ( _|_ ` if ( H e. CH , H , ~H ) ) ) ` A ) = 0h ) ) )
6		eleq1	|- ( A = if ( A e. ~H , A , 0h ) -> ( A e. if ( H e. CH , H , ~H ) <-> if ( A e. ~H , A , 0h ) e. if ( H e. CH , H , ~H ) ) )
7		fveqeq2	|- ( A = if ( A e. ~H , A , 0h ) -> ( ( ( projh ` ( _|_ ` if ( H e. CH , H , ~H ) ) ) ` A ) = 0h <-> ( ( projh ` ( _|_ ` if ( H e. CH , H , ~H ) ) ) ` if ( A e. ~H , A , 0h ) ) = 0h ) )
8	6 7	bibi12d	|- ( A = if ( A e. ~H , A , 0h ) -> ( ( A e. if ( H e. CH , H , ~H ) <-> ( ( projh ` ( _|_ ` if ( H e. CH , H , ~H ) ) ) ` A ) = 0h ) <-> ( if ( A e. ~H , A , 0h ) e. if ( H e. CH , H , ~H ) <-> ( ( projh ` ( _|_ ` if ( H e. CH , H , ~H ) ) ) ` if ( A e. ~H , A , 0h ) ) = 0h ) ) )
9		ifchhv	|- if ( H e. CH , H , ~H ) e. CH
10		ifhvhv0	|- if ( A e. ~H , A , 0h ) e. ~H
11	9 10	pjoc1i	|- ( if ( A e. ~H , A , 0h ) e. if ( H e. CH , H , ~H ) <-> ( ( projh ` ( _|_ ` if ( H e. CH , H , ~H ) ) ) ` if ( A e. ~H , A , 0h ) ) = 0h )
12	5 8 11	dedth2h	|- ( ( H e. CH /\ A e. ~H ) -> ( A e. H <-> ( ( projh ` ( _|_ ` H ) ) ` A ) = 0h ) )