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

Metamath Proof Explorer

Theorem pjnorm2

Description: A vector belongs to the subspace of a projection iff the norm of its projection equals its norm. This and pjch yield Theorem 26.3 of Halmos p. 44. (Contributed by NM, 7-Apr-2001) (New usage is discouraged.)

		Ref	Expression
	Assertion	pjnorm2	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to (A \in H \leftrightarrow {norm}_{ℎ} ({proj}_{ℎ} (H) (A)) = {norm}_{ℎ} (A))$

Proof

Step	Hyp	Ref	Expression
1		pjhcl	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (H) (A) \in ℋ$
2		normcl	$⊢ {proj}_{ℎ} (H) (A) \in ℋ \to {norm}_{ℎ} ({proj}_{ℎ} (H) (A)) \in ℝ$
3	1 2	syl	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {norm}_{ℎ} ({proj}_{ℎ} (H) (A)) \in ℝ$
4		normcl	$⊢ A \in ℋ \to {norm}_{ℎ} (A) \in ℝ$
5	4	adantl	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {norm}_{ℎ} (A) \in ℝ$
6	3 5	eqleltd	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to ({norm}_{ℎ} ({proj}_{ℎ} (H) (A)) = {norm}_{ℎ} (A) \leftrightarrow ({norm}_{ℎ} ({proj}_{ℎ} (H) (A)) \leq {norm}_{ℎ} (A) \land \neg {norm}_{ℎ} ({proj}_{ℎ} (H) (A)) < {norm}_{ℎ} (A)))$
7		pjnorm	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {norm}_{ℎ} ({proj}_{ℎ} (H) (A)) \leq {norm}_{ℎ} (A)$
8	7	biantrurd	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to (\neg {norm}_{ℎ} ({proj}_{ℎ} (H) (A)) < {norm}_{ℎ} (A) \leftrightarrow ({norm}_{ℎ} ({proj}_{ℎ} (H) (A)) \leq {norm}_{ℎ} (A) \land \neg {norm}_{ℎ} ({proj}_{ℎ} (H) (A)) < {norm}_{ℎ} (A)))$
9		pjnel	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to (\neg A \in H \leftrightarrow {norm}_{ℎ} ({proj}_{ℎ} (H) (A)) < {norm}_{ℎ} (A))$
10	9	con1bid	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to (\neg {norm}_{ℎ} ({proj}_{ℎ} (H) (A)) < {norm}_{ℎ} (A) \leftrightarrow A \in H)$
11	6 8 10	3bitr2rd	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to (A \in H \leftrightarrow {norm}_{ℎ} ({proj}_{ℎ} (H) (A)) = {norm}_{ℎ} (A))$