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 )