LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

$span {v} = {λ v : λ \in F}$ , which is ${0_{V}}$ when $v = 0_{V}$ , and when $v \neq 0_{V}$ contains $0_{V}$ only as the multiple $0_{F} v$

Statement

Let $V$ be a vector space over a field $F$ (Vector space over a field) and let $v \in V$ . Write $F v : = {λ v : λ \in F}$ . Then:

$span {v} = F v$ ;
if $v = 0_{V}$ then $span {v} = {0_{V}}$ ;
if $v \neq 0_{V}$ then, for $λ, μ \in F$ , $λ v = μ v$ holds only when $λ = μ$ ; in particular $λ v = 0_{V}$ holds only for $λ = 0_{F}$ , so $0_{V}$ occurs in $span {v}$ only as the multiple $0_{F} v$ , and $span {v} \neq {0_{V}}$ .

Facts & Assumptions

Given: A field $F$ , a vector space $V$ over $F$ , and a vector $v \in V$ .

[L1]

$span {v}$ is a linear subspace of $V$ containing $v$ , and it is contained in every linear subspace of $V$ containing $v$ (Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ ).

[L2]

A linear subspace is closed under scalar multiplication, by condition (W3) (Linear subspace of a vector space).

[L3]

One-step test: a nonempty $T \subseteq V$ with $λ u + w \in T$ for all $λ \in F$ and $u, w \in T$ is a linear subspace of $V$ (One-step subspace test: a nonempty $W \subseteq V$ is a linear subspace if and only if $λ u + v \in W$ for all $λ \in F$ and $u, v \in W$ ).

[L4]

The vector space axioms (Vector space over a field): (V3) $(λ + μ) w = λ w + μ w$ ; (V4) $(λ μ) w = λ (μ w)$ ; (V5) $1_{F} w = w$ .

[L5]

$0_{F} w = 0_{V}$ and $λ 0_{V} = 0_{V}$ for all $λ \in F$ and $w \in V$ ; $(- λ) w = - (λ w)$ , which is claim 3 there; and if $λ w = 0_{V}$ then $λ = 0_{F}$ or $w = 0_{V}$ (In any vector space $0_{F} v = 0_{V}$ , $λ 0_{V} = 0_{V}$ , $(- λ) v = - (λ v)$ , $(- 1_{F}) v = - v$ , and $λ v = 0_{V}$ forces $λ = 0_{F}$ or $v = 0_{V}$ ).

[L6]

$F$ is a field, so $(F, +, 0_{F})$ is an abelian group with $0_{F}, 1_{F} \in F$ and an additive inverse $- μ$ for each $μ$ ; adding $μ$ to both sides of $λ + (- μ) = 0_{F}$ therefore gives $λ = μ$ (Field).

Proof

technique · direct

1.1

$F v$ is nonempty, since $0_{F} v = 0_{V}$ lies in it.

1.2

$F v$ is closed under the one-step expression: for $λ, μ, ν \in F$ , $λ (μ v) + ν v = (λ μ) v + ν v = (λ μ + ν) v \in F v$ , by (V4) and (V3).

1.3

$v \in F v$ , since $v = 1_{F} v$ by (V5).

1.4

If $W$ is a linear subspace of $V$ with $v \in W$ , then $λ v \in W$ for every $λ \in F$ , so $F v \subseteq W$ .

1.5

If $λ v = μ v$ then $0_{V} = λ v + (- (μ v)) = λ v + (- μ) v = (λ + (- μ)) v$ , using claim 3 of the elementary consequences and (V3); so $λ + (- μ) = 0_{F}$ or $v = 0_{V}$ .

L4L5

2.1

$F v$ is a linear subspace of $V$ containing $v$ , by the one-step test.

step 1.1step 1.2step 1.3L3

2.2

If $v \neq 0_{V}$ and $λ v = μ v$ , then step 1.5 forces $λ + (- μ) = 0_{F}$ , that is $λ = μ$ ; taking $μ = 0_{F}$ and using $0_{F} v = 0_{V}$ gives that $λ v = 0_{V}$ only for $λ = 0_{F}$ .

step 1.5L5L6

3.1

$span {v} = F v$ : the span is contained in $F v$ because $F v$ is a linear subspace containing $v$ , and $F v$ is contained in the span because the span is a linear subspace containing $v$ . This is claim 1.

step 2.1step 1.4L1

4.1

If $v = 0_{V}$ then every scalar multiple is $λ 0_{V} = 0_{V}$ , so $F v = {0_{V}}$ ; combined with claim 1 this is claim 2.

step 3.1L5

4.2

Suppose $v \neq 0_{V}$ . Then $λ v = μ v$ forces $λ = μ$ , and $λ v = 0_{V}$ forces $λ = 0_{F}$ ; moreover $v = 1_{F} v$ lies in $F v$ , which is $span {v}$ by claim 1, and $v \neq 0_{V}$ , so $span {v} \neq {0_{V}}$ . This is claim 3.

step 2.2step 3.1L4

5.1

Claims 1, 2 and 3 are steps 3.1, 4.1 and 4.2.

step 3.1step 4.1step 4.2∎

Remarks

The set $F v$ is what a "line through the origin" is, over any field. Claim 3 says that for $v \neq 0_{V}$ the scalars are recovered from the multiples: distinct scalars give distinct vectors. That is the first place where claim 5 of In any vector space $0_{F} v = 0_{V}$ , $λ 0_{V} = 0_{V}$ , $(- λ) v = - (λ v)$ , $(- 1_{F}) v = - v$ , and $λ v = 0_{V}$ forces $λ = 0_{F}$ or $v = 0_{V}$ does real work, and it is what makes a single nonzero vector behave like a coordinate axis.
The word "line" is informal here. Dimension is not available on this page, so nothing above asserts that $span {v}$ is one-dimensional; what is asserted is exactly the three displayed claims. The companion page uses the word in the same informal way, for the same sets.
The zero vector is not an exception to claim 1, only to claim 3. At $v = 0_{V}$ the set $F v$ collapses to ${0_{V}}$ and the map $λ \mapsto λ v$ is constant, so no scalar is recoverable. This is why claim 3 carries the hypothesis $v \neq 0_{V}$ and claim 1 does not.

Depends on

Used by

Dependency tree · two levels

20 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Linear span (Wikipedia) (standard reference, not scraped)
S. Axler, Linear Algebra Done Right, 4th ed., Ch. 2 (standard reference, not scraped)

span⁡{v}={ λv:λ∈F }span{v}={λv:λ∈F}, which is {0V}{0V​} when v=0Vv=0V​, and when v≠0Vv=0V​ contains 0V0V​ only as the multiple 0Fv0F​v