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

Metamath Proof Explorer

Theorem axpjpj

Description: Decomposition of a vector into projections. See comment in axpjcl . (Contributed by NM, 26-Oct-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to H \in C_{ℋ}$
2		pjhth	$⊢ H \in C_{ℋ} \to H +_{ℋ} ⊥ (H) = ℋ$
3	2	eleq2d	$⊢ H \in C_{ℋ} \to (A \in (H +_{ℋ} ⊥ (H)) \leftrightarrow A \in ℋ)$
4	3	biimpar	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to A \in (H +_{ℋ} ⊥ (H))$
5	1 4	pjpjpre	$⊢ (H \in C_{ℋ} \land A \in ℋ) \to A = {proj}_{ℎ} (H) (A) +_{ℎ} {proj}_{ℎ} (⊥ (H)) (A)$