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	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → 𝐻 ∈ Cℋ )
2		pjhth	⊢ ( 𝐻 ∈ Cℋ → ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) = ℋ )
3	2	eleq2d	⊢ ( 𝐻 ∈ Cℋ → ( 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) ↔ 𝐴 ∈ ℋ ) )
4	3	biimpar	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → 𝐴 ∈ ( 𝐻 +ℋ ( ⊥ ‘ 𝐻 ) ) )
5	1 4	pjpjpre	⊢ ( ( 𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ ) → 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) )