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

Metamath Proof Explorer

Theorem pjoc2i

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

Ref Expression
Hypotheses pjoc2.1 
|- H e. CH
pjoc2.2 
|- A e. ~H
Assertion pjoc2i 
|- ( A e. ( _|_ ` H ) <-> ( ( projh ` H ) ` A ) = 0h )

Proof

Step Hyp Ref Expression
1 pjoc2.1 
 |-  H e. CH
2 pjoc2.2 
 |-  A e. ~H
3 1 choccli 
 |-  ( _|_ ` H ) e. CH
4 3 2 pjoc1i 
 |-  ( A e. ( _|_ ` H ) <-> ( ( projh ` ( _|_ ` ( _|_ ` H ) ) ) ` A ) = 0h )
5 1 pjococi 
 |-  ( _|_ ` ( _|_ ` H ) ) = H
6 5 fveq2i 
 |-  ( projh ` ( _|_ ` ( _|_ ` H ) ) ) = ( projh ` H )
7 6 fveq1i 
 |-  ( ( projh ` ( _|_ ` ( _|_ ` H ) ) ) ` A ) = ( ( projh ` H ) ` A )
8 7 eqeq1i 
 |-  ( ( ( projh ` ( _|_ ` ( _|_ ` H ) ) ) ` A ) = 0h <-> ( ( projh ` H ) ` A ) = 0h )
9 4 8 bitri 
 |-  ( A e. ( _|_ ` H ) <-> ( ( projh ` H ) ` A ) = 0h )