HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version

Axiom ax-hvmul0 8880
Description: Scalar multiplication by zero. We can derive the existence of the negative of a vector from this axiom (see hvsubidt 8895 and hvsubvalt 8886).
Assertion
Ref Expression
ax-hvmul0 |- (A e. H~ -> (0 .h A) = 0h)

Detailed syntax breakdown of Axiom ax-hvmul0
StepHypRef Expression
1 cA . . 3 class A
2 chil 8788 . . 3 class H~
31, 2wcel 958 . 2 wff A e. H~
4 cc0 5234 . . . 4 class 0
5 csm 8790 . . . 4 class .h
64, 1, 5co 3963 . . 3 class (0 .h A)
7 c0v 8791 . . 3 class 0h
86, 7wceq 956 . 2 wff (0 .h A) = 0h
93, 8wi 3 1 wff (A e. H~ -> (0 .h A) = 0h)
Colors of variables: wff set class
This axiom is referenced by:  hvmul0t 8893  hvmul0ort 8894  hvsubidt 8895  hi01t 8962  h1de2ctlem 9478  spansneleq 9493  h1datom 9504
Copyright terms: Public domain