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

Metamath Proof Explorer

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