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

Metamath Proof Explorer

Theorem pjpji

Description: Decomposition of a vector into projections. (Contributed by NM, 6-Nov-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjpj.1 ⊢ 𝐻 ∈ Cℋ
pjpj.2 ⊢ 𝐴 ∈ ℋ
Assertion pjpji 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 pjpj.1 ⊢ 𝐻 ∈ Cℋ
2 pjpj.2 ⊢ 𝐴 ∈ ℋ
3 1 2 pjpj0i ⊢ 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) )