Description: Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid and hvsubval ). (Contributed by NM, 29-May-1999) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-hvmul0 | |- ( A e. ~H -> ( 0 .h A ) = 0h ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | |- A |
|
| 1 | chba | |- ~H |
|
| 2 | 0 1 | wcel | |- A e. ~H |
| 3 | cc0 | |- 0 |
|
| 4 | csm | |- .h |
|
| 5 | 3 0 4 | co | |- ( 0 .h A ) |
| 6 | c0v | |- 0h |
|
| 7 | 5 6 | wceq | |- ( 0 .h A ) = 0h |
| 8 | 2 7 | wi | |- ( A e. ~H -> ( 0 .h A ) = 0h ) |