Metamath Proof Explorer

Theorem pjaddi

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∈Cℋ
Assertion pjaddi ⊢A∈ℋ∧B∈ℋ→projℎ⁡H⁡A+ℎB=projℎ⁡H⁡A+ℎprojℎ⁡H⁡B

Proof

Step Hyp Ref Expression
1 pjadjt.1 ⊢H∈Cℋ
2 fvoveq1 ⊢A=ifA∈ℋA0ℎ→projℎ⁡H⁡A+ℎB=projℎ⁡H⁡ifA∈ℋA0ℎ+ℎB
3 fveq2 ⊢A=ifA∈ℋA0ℎ→projℎ⁡H⁡A=projℎ⁡H⁡ifA∈ℋA0ℎ
4 3 oveq1d ⊢A=ifA∈ℋA0ℎ→projℎ⁡H⁡A+ℎprojℎ⁡H⁡B=projℎ⁡H⁡ifA∈ℋA0ℎ+ℎprojℎ⁡H⁡B
5 2 4 eqeq12d ⊢A=ifA∈ℋA0ℎ→projℎ⁡H⁡A+ℎB=projℎ⁡H⁡A+ℎprojℎ⁡H⁡B↔projℎ⁡H⁡ifA∈ℋA0ℎ+ℎB=projℎ⁡H⁡ifA∈ℋA0ℎ+ℎprojℎ⁡H⁡B
6 oveq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ+ℎB=ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ
7 6 fveq2d ⊢B=ifB∈ℋB0ℎ→projℎ⁡H⁡ifA∈ℋA0ℎ+ℎB=projℎ⁡H⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ
8 fveq2 ⊢B=ifB∈ℋB0ℎ→projℎ⁡H⁡B=projℎ⁡H⁡ifB∈ℋB0ℎ
9 8 oveq2d ⊢B=ifB∈ℋB0ℎ→projℎ⁡H⁡ifA∈ℋA0ℎ+ℎprojℎ⁡H⁡B=projℎ⁡H⁡ifA∈ℋA0ℎ+ℎprojℎ⁡H⁡ifB∈ℋB0ℎ
10 7 9 eqeq12d ⊢B=ifB∈ℋB0ℎ→projℎ⁡H⁡ifA∈ℋA0ℎ+ℎB=projℎ⁡H⁡ifA∈ℋA0ℎ+ℎprojℎ⁡H⁡B↔projℎ⁡H⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ=projℎ⁡H⁡ifA∈ℋA0ℎ+ℎprojℎ⁡H⁡ifB∈ℋB0ℎ
11 ifhvhv0 ⊢ifA∈ℋA0ℎ∈ℋ
12 ifhvhv0 ⊢ifB∈ℋB0ℎ∈ℋ
13 1 11 12 pjaddii ⊢projℎ⁡H⁡ifA∈ℋA0ℎ+ℎifB∈ℋB0ℎ=projℎ⁡H⁡ifA∈ℋA0ℎ+ℎprojℎ⁡H⁡ifB∈ℋB0ℎ
14 5 10 13 dedth2h ⊢A∈ℋ∧B∈ℋ→projℎ⁡H⁡A+ℎB=projℎ⁡H⁡A+ℎprojℎ⁡H⁡B