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

Metamath Proof Explorer

Theorem pjvec

Description: The set of vectors belonging to the subspace of a projection. Part of Theorem 26.2 of Halmos p. 44. (Contributed by NM, 11-Apr-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	pjvec	$⊢ H \in C_{ℋ} \to H = \{x \in ℋ \| {proj}_{ℎ} (H) (x) = x\}$

Proof

Step	Hyp	Ref	Expression
1		chss	$⊢ H \in C_{ℋ} \to H \subseteq ℋ$
2		sseqin2	$⊢ H \subseteq ℋ \leftrightarrow ℋ \cap H = H$
3	1 2	sylib	$⊢ H \in C_{ℋ} \to ℋ \cap H = H$
4		pjch	$⊢ (H \in C_{ℋ} \land x \in ℋ) \to (x \in H \leftrightarrow {proj}_{ℎ} (H) (x) = x)$
5	4	rabbi2dva	$⊢ H \in C_{ℋ} \to ℋ \cap H = \{x \in ℋ \| {proj}_{ℎ} (H) (x) = x\}$
6	3 5	eqtr3d	$⊢ H \in C_{ℋ} \to H = \{x \in ℋ \| {proj}_{ℎ} (H) (x) = x\}$