Metamath Proof Explorer

Theorem pjaddii

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

Ref Expression
Hypotheses pjidm.1 ⊢ 𝐻 ∈ Cℋ
pjidm.2 ⊢ 𝐴 ∈ ℋ
pjadj.3 ⊢ 𝐵 ∈ ℋ
Assertion pjaddii ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 pjidm.1 ⊢ 𝐻 ∈ Cℋ
2 pjidm.2 ⊢ 𝐴 ∈ ℋ
3 pjadj.3 ⊢ 𝐵 ∈ ℋ
4 1 2 pjpji ⊢ 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) )
5 1 3 pjpji ⊢ 𝐵 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) )
6 4 5 oveq12i ⊢ ( 𝐴 +ℎ 𝐵 ) = ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) +ℎ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) )
7 1 2 pjhclii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ
8 1 choccli ⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ
9 8 2 pjhclii ⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ℋ
10 1 3 pjhclii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ∈ ℋ
11 8 3 pjhclii ⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ∈ ℋ
12 7 9 10 11 hvadd4i ⊢ ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) +ℎ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) ) = ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) +ℎ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) )
13 6 12 eqtri ⊢ ( 𝐴 +ℎ 𝐵 ) = ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) +ℎ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) )
14 13 fveq2i ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) +ℎ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) ) )
15 1 chshii ⊢ 𝐻 ∈ Sℋ
16 1 2 pjclii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻
17 1 3 pjclii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ∈ 𝐻
18 shaddcl ⊢ ( ( 𝐻 ∈ Sℋ ∧ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 ∧ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ∈ 𝐻 ) → ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) ∈ 𝐻 )
19 15 16 17 18 mp3an ⊢ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) ∈ 𝐻
20 8 chshii ⊢ ( ⊥ ‘ 𝐻 ) ∈ Sℋ
21 8 2 pjclii ⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 )
22 8 3 pjclii ⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ∈ ( ⊥ ‘ 𝐻 )
23 shaddcl ⊢ ( ( ( ⊥ ‘ 𝐻 ) ∈ Sℋ ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) ∈ ( ⊥ ‘ 𝐻 ) )
24 20 21 22 23 mp3an ⊢ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) ∈ ( ⊥ ‘ 𝐻 )
25 1 pjcompi ⊢ ( ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) ∈ 𝐻 ∧ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) +ℎ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) )
26 19 24 25 mp2an ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) ) +ℎ ( ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐵 ) ) ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) )
27 14 26 eqtri ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐴 +ℎ 𝐵 ) ) = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐵 ) )