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