| Hilbert Space Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubid 11365 and hvsubval 11356). |
| Ref | Expression |
|---|---|
| ax-hvmul0 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA |
. . 3
| |
| 2 | chil 11258 |
. . 3
| |
| 3 | 1, 2 | wcel 1588 |
. 2
|
| 4 | cc0 6752 |
. . . 4
| |
| 5 | csm 11260 |
. . . 4
| |
| 6 | 4, 1, 5 | co 4981 |
. . 3
|
| 7 | c0v 11261 |
. . 3
| |
| 8 | 6, 7 | wceq 1586 |
. 2
|
| 9 | 3, 8 | wi 3 |
1
|
| Colors of variables: wff set class |
| This axiom is referenced by: hvmul0 11363 hvmul0or 11364 hvsubid 11365 hi01 11432 h1de2ctlem 11945 spansneleq 11960 h1datomi 11971 |