# Metamath Proof Explorer

Description: Projection of vector sum is sum of projections. (Contributed by NM, 14-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypothesis pjadjt.1 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
Assertion pjaddi ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}{+}_{ℎ}{B}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)$

### Proof

Step Hyp Ref Expression
1 pjadjt.1 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
2 fvoveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}{+}_{ℎ}{B}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)$
3 fveq2 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
4 3 oveq1d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)$
5 2 4 eqeq12d ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}{+}_{ℎ}{B}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)↔{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)\right)$
6 oveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
7 6 fveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
8 fveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
9 8 oveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
10 7 9 eqeq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}{B}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)↔{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)$
11 ifhvhv0 ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in ℋ$
12 ifhvhv0 ${⊢}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\in ℋ$
13 1 11 12 pjaddii ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right){+}_{ℎ}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
14 5 10 13 dedth2h ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}{+}_{ℎ}{B}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)$