Metamath Proof Explorer


Theorem pjsumi

Description: The projection on a subspace sum is the sum of the projections. (Contributed by NM, 11-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjsumt.1 G C
pjsumt.2 H C
Assertion pjsumi A G H proj 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 5 adantl A G H proj G + H A = proj G H A
7 pjcjt2 G C H C A G H proj G H A = proj G A + proj H A
8 1 2 7 mp3an12 A G H proj G H A = proj G A + proj H A
9 8 imp A G H proj G H A = proj G A + proj H A
10 6 9 eqtrd A G H proj G + H A = proj G A + proj H A
11 10 ex A G H proj G + H A = proj G A + proj H A