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 )