Description: The projection of the zero vector. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | pj0.1 | ||
Assertion | pj0i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pj0.1 | ||
2 | 1 | chshii | |
3 | oc0 | ||
4 | 2 3 | ax-mp | |
5 | ax-hv0cl | ||
6 | 1 5 | pjoc2i | |
7 | 4 6 | mpbi |