Metamath Proof Explorer

Theorem pjoc2

Description: Projection of a vector in the orthocomplement of the projection subspace. Lemma 4.4(iii) of Beran p. 111. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

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

Proof

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