This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 C_{ℋ}$
	Assertion	pj0i	$⊢ {proj}_{ℎ} (H) (0_{ℎ}) = 0_{ℎ}$

Step	Hyp	Ref	Expression
1		pj0.1	$⊢ H \in C_{ℋ}$
2	1	chshii	$⊢ H \in S_{ℋ}$
3		oc0	$⊢ H \in S_{ℋ} \to 0_{ℎ} \in ⊥ (H)$
4	2 3	ax-mp	$⊢ 0_{ℎ} \in ⊥ (H)$
5		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
6	1 5	pjoc2i	$⊢ 0_{ℎ} \in ⊥ (H) \leftrightarrow {proj}_{ℎ} (H) (0_{ℎ}) = 0_{ℎ}$
7	4 6	mpbi	$⊢ {proj}_{ℎ} (H) (0_{ℎ}) = 0_{ℎ}$