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.1L5

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

1.2L4

$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.3L4

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

1.4L2

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.5L4L5

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}$ .

2.1step 1.1step 1.2step 1.3L3

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

2.2step 1.5L5L6

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}$ .

3.1step 2.1step 1.4L1

$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.

4.1step 3.1L5

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.

4.2step 2.2step 3.1L4

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.

5.1step 3.1step 4.1step 4.2∎

Claims 1, 2 and 3 are steps 3.1, 4.1 and 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.

$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

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

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

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

$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$