LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

$\operatorname{span}\{v\} = \{\, \lambda v : \lambda \in F \,\}$ , which is $\{0_V\}$ when $v = 0_V$ , and when $v \ne 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 $Fv := \{\, \lambda v : \lambda \in F \,\}$ . Then:

$\operatorname{span}\{v\} = Fv$ ;
if $v = 0_V$ then $\operatorname{span}\{v\} = \{0_V\}$ ;
if $v \ne 0_V$ then, for $\lambda, \mu \in F$ , $\lambda v = \mu v$ holds only when $\lambda = \mu$ ; in particular $\lambda v = 0_V$ holds only for $\lambda = 0_F$ , so $0_V$ occurs in $\operatorname{span}\{v\}$ only as the multiple $0_F v$ , and $\operatorname{span}\{v\} \ne \{0_V\}$ .

Facts & Assumptions

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

[L1]

$\operatorname{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 $\operatorname{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 $\lambda u + w \in T$ for all $\lambda \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 $\lambda u + v \in W$ for all $\lambda \in F$ and $u, v \in W$ ).

[L4]

The vector space axioms (Vector space over a field): (V3) $(\lambda+\mu)w = \lambda w + \mu w$ ; (V4) $(\lambda\mu)w = \lambda(\mu w)$ ; (V5) $1_F w = w$ .

[L5]

$0_F w = 0_V$ and $\lambda 0_V = 0_V$ for all $\lambda \in F$ and $w \in V$ ; $(-\lambda)w = -(\lambda w)$ , which is claim 3 there; and if $\lambda w = 0_V$ then $\lambda = 0_F$ or $w = 0_V$ (In any vector space $0_F v = 0_V$ , $\lambda 0_V = 0_V$ , $(-\lambda)v = -(\lambda v)$ , $(-1_F)v = -v$ , and $\lambda v = 0_V$ forces $\lambda = 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 $-\mu$ for each $\mu$ ; adding $\mu$ to both sides of $\lambda + (-\mu) = 0_F$ therefore gives $\lambda = \mu$ (Field).

Proof

technique · direct

1.1

$Fv$ is nonempty, since $0_F v = 0_V$ lies in it.

1.2

$Fv$ is closed under the one-step expression: for $\lambda, \mu, \nu \in F$ , $\lambda(\mu v) + \nu v = (\lambda\mu)v + \nu v = (\lambda\mu + \nu)v \in Fv$ , by (V4) and (V3).

1.3

$v \in Fv$ , since $v = 1_F v$ by (V5).

1.4

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

1.5

If $\lambda v = \mu v$ then $0_V = \lambda v + (-(\mu v)) = \lambda v + (-\mu)v = (\lambda + (-\mu))v$ , using claim 3 of the elementary consequences and (V3); so $\lambda + (-\mu) = 0_F$ or $v = 0_V$ .

L4L5

2.1

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

step 1.1step 1.2step 1.3L3

2.2

If $v \ne 0_V$ and $\lambda v = \mu v$ , then step 1.5 forces $\lambda + (-\mu) = 0_F$ , that is $\lambda = \mu$ ; taking $\mu = 0_F$ and using $0_F v = 0_V$ gives that $\lambda v = 0_V$ only for $\lambda = 0_F$ .

step 1.5L5L6

3.1

$\operatorname{span}\{v\} = Fv$ : the span is contained in $Fv$ because $Fv$ is a linear subspace containing $v$ , and $Fv$ 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 $\lambda 0_V = 0_V$ , so $Fv = \{0_V\}$ ; combined with claim 1 this is claim 2.

step 3.1L5

4.2

Suppose $v \ne 0_V$ . Then $\lambda v = \mu v$ forces $\lambda = \mu$ , and $\lambda v = 0_V$ forces $\lambda = 0_F$ ; moreover $v = 1_F v$ lies in $Fv$ , which is $\operatorname{span}\{v\}$ by claim 1, and $v \ne 0_V$ , so $\operatorname{span}\{v\} \ne \{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 $Fv$ is what a "line through the origin" is, over any field. Claim 3 says that for $v \ne 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$ , $\lambda 0_V = 0_V$ , $(-\lambda)v = -(\lambda v)$ , $(-1_F)v = -v$ , and $\lambda v = 0_V$ forces $\lambda = 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 $\operatorname{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 $Fv$ collapses to $\{0_V\}$ and the map $\lambda \mapsto \lambda v$ is constant, so no scalar is recoverable. This is why claim 3 carries the hypothesis $v \ne 0_V$ and claim 1 does not.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 39 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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 }\operatorname{span}\{v\} = \{\, \lambda v : \lambda \in F \,\}span{v}={λv:λ∈F}, which is {0V}\{0_V\}{0V​} when v=0Vv = 0_Vv=0V​, and when v≠0Vv \ne 0_Vv=0V​ contains 0V0_V0V​ only as the multiple 0Fv0_F v0F​v