Metamath Proof Explorer
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ℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) |