Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-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.

[T(v)]C=[T]BC[v]B[T(v)]_{\mathcal C}=[T]_{\mathcal B}^{\mathcal C}[v]_{\mathcal B}

Statement

Let T:V→WT:V\to W be linear, let B\mathcal B be an ordered basis of VV, and let C\mathcal C be an ordered basis of WW. Then for every v∈Vv\in V,

[T(v)]C=[T]BC[v]B.[T(v)]_{\mathcal C}=[T]_{\mathcal B}^{\mathcal C}[v]_{\mathcal B}.

Facts & Assumptions

Given: Ordered bases B=(bj)j<n\mathcal B=(b_j)_{j<n} and C=(ci)i<m\mathcal C=(c_i)_{i<m}, a linear map T:V→WT:V\to W, and a vector v∈Vv\in V.

[L1]

The coordinate column contains the unique coefficients in the ordered-basis expansion, and the jj-th column of [T]BC[T]_{\mathcal B}^{\mathcal C} is [T(bj)]C[T(b_j)]_{\mathcal C} (Coordinate columns [v]B[v]_{\mathcal B} and matrices [T]BC[T]_{\mathcal B}^{\mathcal C} of linear maps relative to ordered bases).

Proof

technique · direct
1.1

Write [v]B=(xj)j<n[v]_{\mathcal B}=(x_j)_{j<n}, so [L1] gives v=∑j<nxjbjv=\sum_{j<n}x_jb_j.

givenL1
2.1

By linearity, T(v)=∑j<nxjT(bj)T(v)=\sum_{j<n}x_jT(b_j); writing T(bj)=∑i<mtijciT(b_j)=\sum_{i<m}t_{ij}c_i gives T(v)=∑i<m(∑j<ntijxj)ciT(v)=\sum_{i<m}(\sum_{j<n}t_{ij}x_j)c_i.

step 1.1L1
3.1

The inner sum is the ii-th row-by-column entry of [T]BC[v]B[T]_{\mathcal B}^{\mathcal C}[v]_{\mathcal B}, and uniqueness of C\mathcal C-coordinates identifies this column with [T(v)]C[T(v)]_{\mathcal C}.

step 2.1L1∎

Depends on

Used by

Dependency tree · next 3 levels

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