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 ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) )