Theorem pj0i

Description: The projection of the zero vector. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pj0.1	|- H e. CH
Assertion	pj0i	|- ( ( projh ` H ) ` 0h ) = 0h

Proof

Step	Hyp	Ref	Expression
1		pj0.1	|- H e. CH
2	1	chshii	|- H e. SH
3		oc0	|- ( H e. SH -> 0h e. ( _|_ ` H ) )
4	2 3	ax-mp	|- 0h e. ( _|_ ` H )
5		ax-hv0cl	|- 0h e. ~H
6	1 5	pjoc2i	|- ( 0h e. ( _|_ ` H ) <-> ( ( projh ` H ) ` 0h ) = 0h )
7	4 6	mpbi	|- ( ( projh ` H ) ` 0h ) = 0h