Description: The zero vector is in the vector space. (Contributed by NM, 29-May-1999) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | ax-hv0cl | ⊢ 0_{ℎ} ∈ ℋ |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | c0v | ⊢ 0_{ℎ} | |
1 | chba | ⊢ ℋ | |
2 | 0 1 | wcel | ⊢ 0_{ℎ} ∈ ℋ |