Metamath Proof Explorer


Theorem pjdsi

Description: Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 21-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses pjsumt.1 G C
pjsumt.2 H C
Assertion pjdsi A G H G H A = proj G A + proj H A

Proof

Step Hyp Ref Expression
1 pjsumt.1 G C
2 pjsumt.2 H C
3 1 2 osumi G H G + H = G H
4 3 fveq2d G H proj G + H = proj G H
5 4 fveq1d G H proj G + H A = proj G H A
6 1 2 chjcli G H C
7 pjid G H C A G H proj G H A = A
8 6 7 mpan A G H proj G H A = A
9 5 8 sylan9eqr A G H G H proj G + H A = A
10 6 cheli A G H A
11 1 2 pjsumi A G H proj G + H A = proj G A + proj H A
12 11 imp A G H proj G + H A = proj G A + proj H A
13 10 12 sylan A G H G H proj G + H A = proj G A + proj H A
14 9 13 eqtr3d A G H G H A = proj G A + proj H A