This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjsubii

Description: Projection of vector difference is difference of projections. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 ⊢ 𝐻 ∈ Cℋ
pjidm.2 ⊢ 𝐴 ∈ ℋ
pjsub.3 ⊢ 𝐵 ∈ ℋ
Assertion pjsubii ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 pjidm.1 ⊢ 𝐻 ∈ Cℋ
2 pjidm.2 ⊢ 𝐴 ∈ ℋ
3 pjsub.3 ⊢ 𝐵 ∈ ℋ
4 neg1cn ⊢ - 1 ∈ ℂ
5 4 3 hvmulcli ⊢ ( - 1 ·ℎ 𝐵 ) ∈ ℋ
6 1 2 5 pjaddii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( - 1 ·ℎ 𝐵 ) ) )
7 1 3 4 pjmulii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( - 1 ·ℎ 𝐵 ) ) = ( - 1 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) )
8 7 oveq2i ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( - 1 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) )
9 6 8 eqtri ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( - 1 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) )
10 2 3 hvsubvali ⊢ ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) )
11 10 fveq2i ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
12 1 2 pjhclii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ
13 1 3 pjhclii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ∈ ℋ
14 12 13 hvsubvali ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( - 1 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) )
15 9 11 14 3eqtr4i ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 −ℎ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) −ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) )