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\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pj0i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(0_{ℎ}\right)=0_{ℎ}$$

Proof

Step	Hyp	Ref	Expression
1		pj0.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	chshii	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}$$
3		oc0	$$⊢H\in {\mathbf{S}}_{\mathscr{H}}\to 0_{ℎ}\in \perp \left(H\right)$$
4	2 3	ax-mp	$$⊢0_{ℎ}\in \perp \left(H\right)$$
5		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
6	1 5	pjoc2i	$$⊢0_{ℎ}\in \perp \left(H\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(0_{ℎ}\right)=0_{ℎ}$$
7	4 6	mpbi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(0_{ℎ}\right)=0_{ℎ}$$