Theorem pjoccoi

Description: Composition of projections of a subspace and its orthocomplement. (Contributed by NM, 14-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjidmco.1	|- H e. CH
Assertion	pjoccoi	|- ( ( projh ` H ) o. ( projh ` ( _|_ ` H ) ) ) = 0hop

Proof

Step	Hyp	Ref	Expression
1		pjidmco.1	|- H e. CH
2	1	chssii	|- H C_ ~H
3		ococss	|- ( H C_ ~H -> H C_ ( _|_ ` ( _|_ ` H ) ) )
4	1	choccli	|- ( _|_ ` H ) e. CH
5	1 4	pjorthcoi	|- ( H C_ ( _|_ ` ( _|_ ` H ) ) -> ( ( projh ` H ) o. ( projh ` ( _|_ ` H ) ) ) = 0hop )
6	2 3 5	mp2b	|- ( ( projh ` H ) o. ( projh ` ( _|_ ` H ) ) ) = 0hop