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

Metamath Proof Explorer

Theorem pjo

Description: The orthogonal projection. Lemma 4.4(i) of Beran p. 111. (Contributed by NM, 30-Oct-1999) (New usage is discouraged.)

		Ref	Expression
	Assertion	pjo	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (⊥ (H)) (A) = {proj}_{ℎ} (ℋ) (A) -_{ℎ} {proj}_{ℎ} (H) (A)$

Proof

Step	Hyp	Ref	Expression
1		pjch1	$⊢ A \in ℋ \to {proj}_{ℎ} (ℋ) (A) = A$
2	1	adantl	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (ℋ) (A) = A$
3		axpjpj	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to A = {proj}_{ℎ} (H) (A) +_{ℎ} {proj}_{ℎ} (⊥ (H)) (A)$
4	2 3	eqtr2d	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (H) (A) +_{ℎ} {proj}_{ℎ} (⊥ (H)) (A) = {proj}_{ℎ} (ℋ) (A)$
5		helch	$⊢ ℋ \in C_{ℋ}$
6	5	pjcli	$⊢ A \in ℋ \to {proj}_{ℎ} (ℋ) (A) \in ℋ$
7	6	adantl	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (ℋ) (A) \in ℋ$
8		pjhcl	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (H) (A) \in ℋ$
9		choccl	$⊢ H \in C_{ℋ} \to ⊥ (H) \in C_{ℋ}$
10		pjhcl	$⊢ (⊥ (H) \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (⊥ (H)) (A) \in ℋ$
11	9 10	sylan	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (⊥ (H)) (A) \in ℋ$
12		hvsubadd	$⊢ ({proj}_{ℎ} (ℋ) (A) \in ℋ \land {proj}_{ℎ} (H) (A) \in ℋ \land {proj}_{ℎ} (⊥ (H)) (A) \in ℋ) \to ({proj}_{ℎ} (ℋ) (A) -_{ℎ} {proj}_{ℎ} (H) (A) = {proj}_{ℎ} (⊥ (H)) (A) \leftrightarrow {proj}_{ℎ} (H) (A) +_{ℎ} {proj}_{ℎ} (⊥ (H)) (A) = {proj}_{ℎ} (ℋ) (A))$
13	7 8 11 12	syl3anc	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to ({proj}_{ℎ} (ℋ) (A) -_{ℎ} {proj}_{ℎ} (H) (A) = {proj}_{ℎ} (⊥ (H)) (A) \leftrightarrow {proj}_{ℎ} (H) (A) +_{ℎ} {proj}_{ℎ} (⊥ (H)) (A) = {proj}_{ℎ} (ℋ) (A))$
14	4 13	mpbird	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (ℋ) (A) -_{ℎ} {proj}_{ℎ} (H) (A) = {proj}_{ℎ} (⊥ (H)) (A)$
15	14	eqcomd	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (⊥ (H)) (A) = {proj}_{ℎ} (ℋ) (A) -_{ℎ} {proj}_{ℎ} (H) (A)$