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

Metamath Proof Explorer

Theorem pjmuli

Description: Projection of scalar product is scalar product of projection. (Contributed by NM, 26-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypothesis pjadjt.1 ⊢ H ∈ C ℋ
Assertion pjmuli ⊢ A ∈ ℂ ∧ B ∈ ℋ → proj ℎ ⁡ H ⁡ A ⋅ ℎ B = A ⋅ ℎ proj ℎ ⁡ H ⁡ B

Proof

Step Hyp Ref Expression
1 pjadjt.1 ⊢ H ∈ C ℋ
2 fvoveq1 ⊢ A = if A ∈ ℂ A 0 → proj ℎ ⁡ H ⁡ A ⋅ ℎ B = proj ℎ ⁡ H ⁡ if A ∈ ℂ A 0 ⋅ ℎ B
3 oveq1 ⊢ A = if A ∈ ℂ A 0 → A ⋅ ℎ proj ℎ ⁡ H ⁡ B = if A ∈ ℂ A 0 ⋅ ℎ proj ℎ ⁡ H ⁡ B
4 2 3 eqeq12d ⊢ A = if A ∈ ℂ A 0 → proj ℎ ⁡ H ⁡ A ⋅ ℎ B = A ⋅ ℎ proj ℎ ⁡ H ⁡ B ↔ proj ℎ ⁡ H ⁡ if A ∈ ℂ A 0 ⋅ ℎ B = if A ∈ ℂ A 0 ⋅ ℎ proj ℎ ⁡ H ⁡ B
5 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℂ A 0 ⋅ ℎ B = if A ∈ ℂ A 0 ⋅ ℎ if B ∈ ℋ B 0 ℎ
6 5 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → proj ℎ ⁡ H ⁡ if A ∈ ℂ A 0 ⋅ ℎ B = proj ℎ ⁡ H ⁡ if A ∈ ℂ A 0 ⋅ ℎ if B ∈ ℋ B 0 ℎ
7 fveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → proj ℎ ⁡ H ⁡ B = proj ℎ ⁡ H ⁡ if B ∈ ℋ B 0 ℎ
8 7 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℂ A 0 ⋅ ℎ proj ℎ ⁡ H ⁡ B = if A ∈ ℂ A 0 ⋅ ℎ proj ℎ ⁡ H ⁡ if B ∈ ℋ B 0 ℎ
9 6 8 eqeq12d ⊢ B = if B ∈ ℋ B 0 ℎ → proj ℎ ⁡ H ⁡ if A ∈ ℂ A 0 ⋅ ℎ B = if A ∈ ℂ A 0 ⋅ ℎ proj ℎ ⁡ H ⁡ B ↔ proj ℎ ⁡ H ⁡ if A ∈ ℂ A 0 ⋅ ℎ if B ∈ ℋ B 0 ℎ = if A ∈ ℂ A 0 ⋅ ℎ proj ℎ ⁡ H ⁡ if B ∈ ℋ B 0 ℎ
10 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
11 0cn ⊢ 0 ∈ ℂ
12 11 elimel ⊢ if A ∈ ℂ A 0 ∈ ℂ
13 1 10 12 pjmulii ⊢ proj ℎ ⁡ H ⁡ if A ∈ ℂ A 0 ⋅ ℎ if B ∈ ℋ B 0 ℎ = if A ∈ ℂ A 0 ⋅ ℎ proj ℎ ⁡ H ⁡ if B ∈ ℋ B 0 ℎ
14 4 9 13 dedth2h ⊢ A ∈ ℂ ∧ B ∈ ℋ → proj ℎ ⁡ H ⁡ A ⋅ ℎ B = A ⋅ ℎ proj ℎ ⁡ H ⁡ B