PropositionStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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.

$\mathcal L(V,W)$ is a vector space over the common scalar field

Statement

If $V$ and $W$ are vector spaces over a field $F$ , then $\mathcal L(V,W)$ is a vector space over $F$ under pointwise addition and scalar multiplication.

Facts & Assumptions

Given: Vector spaces $V,W$ over the same field $F$ and the pointwise operations on $\mathcal L(V,W)$ .

[L1]

$\mathcal L(V,W)$ is the set of linear maps, with pointwise addition and scalar multiplication (The space $\mathcal L(V,W)$ of linear maps with pointwise addition and scalar multiplication).

Proof

technique · direct

1.1

If $S,T$ are linear, then $(S+T)(au+bv)=a(S+T)(u)+b(S+T)(v)$ , and if $\lambda\in F$ , then $(\lambda T)(au+bv)=a(\lambda T)(u)+b(\lambda T)(v)$ ; hence the pointwise operations remain inside $\mathcal L(V,W)$ .

givenL1

2.1

Evaluating at an arbitrary $v\in V$ reduces associativity, commutativity, both distributive laws, scalar associativity, and the scalar identity law to the corresponding vector-space laws in $W$ .

step 1.1L1

3.1

The zero function is the additive identity and $(-T)(v):=-T(v)$ is the additive inverse of $T$ . The same formulas cover the zero domain and zero codomain, so all vector-space axioms hold.

step 2.1L1∎

Depends on

Used by

Cited to discharge well-definedness by The space mathcal L(V,W) of linear maps with pointwise addition and scalar multiplication.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 13 results over 12 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

S. Schiavone, MIT 18.700 Day 9, Proposition 26 (standard reference, not scraped)

L(V,W)\mathcal L(V,W)L(V,W) is a vector space over the common scalar field