Metamath Proof Explorer


Theorem pjsubi

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

Ref Expression
Hypothesis pjadjt.1 𝐻C
Assertion pjsubi ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( proj𝐻 ) ‘ ( 𝐴 𝐵 ) ) = ( ( ( proj𝐻 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 pjadjt.1 𝐻C
2 fvoveq1 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( proj𝐻 ) ‘ ( 𝐴 𝐵 ) ) = ( ( proj𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) ) )
3 fveq2 ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( proj𝐻 ) ‘ 𝐴 ) = ( ( proj𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) )
4 3 oveq1d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( ( proj𝐻 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐵 ) ) = ( ( ( proj𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) − ( ( proj𝐻 ) ‘ 𝐵 ) ) )
5 2 4 eqeq12d ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) → ( ( ( proj𝐻 ) ‘ ( 𝐴 𝐵 ) ) = ( ( ( proj𝐻 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐵 ) ) ↔ ( ( proj𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) ) = ( ( ( proj𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) − ( ( proj𝐻 ) ‘ 𝐵 ) ) ) )
6 oveq2 ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) )
7 6 fveq2d ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( ( proj𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) ) = ( ( proj𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) )
8 fveq2 ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( ( proj𝐻 ) ‘ 𝐵 ) = ( ( proj𝐻 ) ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) )
9 8 oveq2d ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( ( ( proj𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) − ( ( proj𝐻 ) ‘ 𝐵 ) ) = ( ( ( proj𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) − ( ( proj𝐻 ) ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) )
10 7 9 eqeq12d ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) → ( ( ( proj𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − 𝐵 ) ) = ( ( ( proj𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) − ( ( proj𝐻 ) ‘ 𝐵 ) ) ↔ ( ( proj𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) = ( ( ( proj𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) − ( ( proj𝐻 ) ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) ) )
11 ifhvhv0 if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ∈ ℋ
12 ifhvhv0 if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ∈ ℋ
13 1 11 12 pjsubii ( ( proj𝐻 ) ‘ ( if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) − if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) ) = ( ( ( proj𝐻 ) ‘ if ( 𝐴 ∈ ℋ , 𝐴 , 0 ) ) − ( ( proj𝐻 ) ‘ if ( 𝐵 ∈ ℋ , 𝐵 , 0 ) ) )
14 5 10 13 dedth2h ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( proj𝐻 ) ‘ ( 𝐴 𝐵 ) ) = ( ( ( proj𝐻 ) ‘ 𝐴 ) − ( ( proj𝐻 ) ‘ 𝐵 ) ) )