PropositionStatement: Literature-sourcedProof: AI-generatedprecheck 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.

$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 $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 $L (V, W)$ .

[L1]

$L (V, W)$ is the set of linear maps, with pointwise addition and scalar multiplication (The space $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) (a u + b v) = a (S + T) (u) + b (S + T) (v)$ , and if $λ \in F$ , then $(λ T) (a u + b v) = a (λ T) (u) + b (λ T) (v)$ ; hence the pointwise operations remain inside $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

End_F(V) is a ring and matrix representation is a ring isomorphism End_F(V)≅ Mₙ(F) Corollary
A regular module with bases of sizes one and two Counterexample
Hom_G(V,W) is a k-vector space and End_G(V) is a k-algebra Proposition
T↦[T]_B^C is a vector-space isomorphism L(V,W)≅ M_m× n(F) Theorem

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

Dependency tree · two levels

10 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

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

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