LemmaStatement: 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.

Identity maps and composites of linear maps are linear

Statement

The identity map of a vector space is linear. If $T : U \to V$ and $S : V \to W$ are linear maps over the same field, then $S \circ T : U \to W$ is linear.

Facts & Assumptions

Given: Vector spaces $U, V, W$ over a field $F$ , scalars $a, b \in F$ , vectors $u, v \in U$ , and linear maps $T : U \to V$ and $S : V \to W$ .

[L1]

A map $R$ is linear when $R (a u + b v) = a R (u) + b R (v)$ for all scalars and vectors (Linear map between vector spaces over the same field).

Proof

technique · direct

1.1

The identity satisfies ${id}_{V} (a v + b w) = a v + b w = a {id}_{V} (v) + b {id}_{V} (w)$ , so it is linear.

givenL1

2.1

Linearity of $T$ and then of $S$ gives $S (T (a u + b v)) = S (a T (u) + b T (v)) = a S (T (u)) + b S (T (v))$ .

step 1.1L1

3.1

The equality in step 2.1 is the defining linearity equation for $S \circ T$ , so the composite is linear.

step 2.1L1∎

Depends on

Linear map between vector spaces over the same field

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
Polynomial evaluation at an endomorphism: p(T)=∑ₖ aₖTᵏ Definition
The change-of-basis matrix P_C leftarrowB=[id_V]_B^C Definition
The transpose or algebraic adjoint T^*:W^*→ V^*, T^*(g)=g∘ T, of a linear map T:V→ W Definition
Transpose is linear, sends identities to identities, and reverses composition: (S∘ T)^*=T^*∘ S^* Proposition
[S∘ T]_B^D=[S]_C^D[T]_B^C Theorem

Dependency tree · two levels

3 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. Axler, Linear Algebra Done Right, 4th ed., Chapter 3 (standard reference, not scraped)