Metamath Proof Explorer


Theorem pj0i

Description: The projection of the zero vector. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis pj0.1 H C
Assertion pj0i proj H 0 = 0

Proof

Step Hyp Ref Expression
1 pj0.1 H C
2 1 chshii H S
3 oc0 H S 0 H
4 2 3 ax-mp 0 H
5 ax-hv0cl 0
6 1 5 pjoc2i 0 H proj H 0 = 0
7 4 6 mpbi proj H 0 = 0