Metamath Proof Explorer

Theorem pjmulii

Description: Projection of (scalar) product is product of projection. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 ⊢ 𝐻 ∈ Cℋ
pjidm.2 ⊢ 𝐴 ∈ ℋ
pjmul.3 ⊢ 𝐶 ∈ ℂ
Assertion pjmulii ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐶 ·ℎ 𝐴 ) ) = ( 𝐶 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 pjidm.1 ⊢ 𝐻 ∈ Cℋ
2 pjidm.2 ⊢ 𝐴 ∈ ℋ
3 pjmul.3 ⊢ 𝐶 ∈ ℂ
4 1 2 pjpji ⊢ 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) )
5 4 oveq2i ⊢ ( 𝐶 ·ℎ 𝐴 ) = ( 𝐶 ·ℎ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) )
6 1 2 pjhclii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ
7 1 choccli ⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ
8 7 2 pjhclii ⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ℋ
9 3 6 8 hvdistr1i ⊢ ( 𝐶 ·ℎ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) = ( ( 𝐶 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) +ℎ ( 𝐶 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) )
10 5 9 eqtri ⊢ ( 𝐶 ·ℎ 𝐴 ) = ( ( 𝐶 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) +ℎ ( 𝐶 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) )
11 10 fveq2i ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐶 ·ℎ 𝐴 ) ) = ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝐶 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) +ℎ ( 𝐶 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) )
12 1 chshii ⊢ 𝐻 ∈ Sℋ
13 1 2 pjclii ⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻
14 shmulcl ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐶 ∈ ℂ ∧ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ 𝐻 ) → ( 𝐶 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ 𝐻 )
15 12 3 13 14 mp3an ⊢ ( 𝐶 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ 𝐻
16 7 chshii ⊢ ( ⊥ ‘ 𝐻 ) ∈ Sℋ
17 7 2 pjclii ⊢ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 )
18 shmulcl ⊢ ( ( ( ⊥ ‘ 𝐻 ) ∈ Sℋ ∧ 𝐶 ∈ ℂ ∧ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ∈ ( ⊥ ‘ 𝐻 ) ) → ( 𝐶 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) )
19 16 3 17 18 mp3an ⊢ ( 𝐶 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 )
20 1 pjcompi ⊢ ( ( ( 𝐶 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ∈ 𝐻 ∧ ( 𝐶 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ∈ ( ⊥ ‘ 𝐻 ) ) → ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝐶 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) +ℎ ( 𝐶 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) ) = ( 𝐶 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) )
21 15 19 20 mp2an ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( ( 𝐶 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) +ℎ ( 𝐶 ·ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) ) = ( 𝐶 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) )
22 11 21 eqtri ⊢ ( ( projℎ ‘ 𝐻 ) ‘ ( 𝐶 ·ℎ 𝐴 ) ) = ( 𝐶 ·ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) )