Vector Spaces, Linear Subspaces, Span and Direct Sums

About this page

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.

✓ 10 results · all verified · 9 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

1 · Prerequisites

Abstract Algebra

Real Analysis

Set Theory

2 · Logical flowchart

3 · Items

Definition

A field is a vector space over itself, and over any subfield K ⊆ F every F-vector space is a K-vector space by restricting the scalars

Definition

Linear subspace of a vector space

Lemma

The additive group of a vector space is an abelian group and every linear subspace is a subgroup of it; conversely a subgroup closed under scalar multiplication is a linear subspace

Lemma

V = ⨁_i<n Uᵢ if and only if every v ∈ V is ∑_i<n uᵢ with uᵢ ∈ Uᵢ in exactly one way; equivalently, if and only if the sum is V and ∑_i<n uᵢ = 0_V with uᵢ ∈ Uᵢ forces every uᵢ = 0_V

Sources

Vector Spaces, Linear Subspaces, Span and Direct Sums

3 · Items

Vector space over a field

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

The vector space F^X of all functions X → F with pointwise operations, and Fⁿ as the case X = n = {0, 1, …, n-1}

The vector space M_m × n(F) := F^ m × n of m by n matrices over a field, with entrywise operations

A field is a vector space over itself, and over any subfield K ⊆ F every F-vector space is a K-vector space by restricting the scalars

Linear subspace of a vector space

The additive group of a vector space is an abelian group and every linear subspace is a subgroup of it; conversely a subgroup closed under scalar multiplication is a linear subspace

One-step subspace test: a nonempty W ⊆ V is a linear subspace if and only if λ u + v ∈ W for all λ ∈ F and u, v ∈ W

The intersection of a nonempty family of linear subspaces of V is a linear subspace of V

Linear combination of a finite list, and the span span(S) as the smallest linear subspace containing S

span(S) is exactly the set of linear combinations of finite lists of elements of S, and span(∅) = {0_V}

The span is monotone and idempotent, span(S) = S exactly when S is a linear subspace, and span(S ∪ {0_V}) = span(S)

span{v} = { λ v : λ ∈ F }, which is {0_V} when v = 0_V, and when v ≠ 0_V contains 0_V only as the multiple 0_F v

The sum U + W of two linear subspaces and the sum ∑_i<n Uᵢ of a finite family

∑_i<n Uᵢ = span(⋃_i<n Uᵢ), so the sum is the smallest linear subspace containing every Uᵢ

Internal direct sum V = ⨁_i<n Uᵢ: the sum is everything and each summand meets the sum of the others only in 0_V

V = ⨁_i<n Uᵢ if and only if every v ∈ V is ∑_i<n uᵢ with uᵢ ∈ Uᵢ in exactly one way; equivalently, if and only if the sum is V and ∑_i<n uᵢ = 0_V with uᵢ ∈ Uᵢ forces every uᵢ = 0_V