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.
Extending a basis of the kernel to a basis of the domain gives a basis of the image
Statement
Let be linear, with finite-dimensional over . There are a basis of and a basis of with . For this pair, put . Then is finite, the restriction
is a bijection, and is a basis of .
More explicitly, if and are bijections, then the list obtained by placing before is an ordered basis of , while is an ordered basis of the image.
Facts & Assumptions
Given: Vector spaces over , a linear map , and a finite-dimensional domain .
The kernel and image of a linear map are linear subspaces, and exactly when (The kernel and image are linear subspaces, and a linear map is injective if and only if its kernel is trivial, Kernel and image of a linear map).
A linear subspace of a finite-dimensional vector space is finite-dimensional; every linearly independent subset extends to a basis without a choice principle; and every linearly independent subset of a finite-dimensional space is finite (If and is a linear subspace of , then is finite-dimensional, , and if and only if , claims 1 and 3, If has a spanning set with elements, then every linearly independent subset of is finite with at most elements; in particular has no linearly independent subset equinumerous with ).
A basis is a linearly independent spanning subset. An ordered basis is an injective finite list whose image is a basis, equivalently a linearly independent finite list that spans (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).
Every vector has exactly one coordinate list with respect to an ordered basis (A finite list is an ordered basis if and only if every equals for exactly one ; those scalars are the coordinates of in that ordered basis).
Finite sums in an abelian group have empty value zero and append one term at a successor; induction is valid on their natural-number length. Natural addition satisfies and (The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity, The principle of mathematical induction, Addition of natural numbers).
A linear map satisfies ; vector spaces have the usual zero, inverse, and distributive laws (Linear map between vector spaces over the same field, In any vector space , , , , and forces or ).
A subset of a finite set is finite. If two finite sets are disjoint, then their union has cardinality the sum of their cardinalities; finite cardinality is transported by a bijection (A subset of a finite set is finite, with , and equality holds if and only if , The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition, clause 1, The cardinality of a finite set).
A function is bijective exactly when it is injective and surjective (Injection, surjection, bijection).
Proof
By [L1] and [L2], is finite-dimensional; choose a basis of . It is linearly independent in , so [L2] extends it to a basis of . Put . Since is finite, so is , and .
For every finite list and every scalar list , linearity gives . This follows by induction on : the empty case follows by applying [L6] to and cancelling, and the successor step uses the append recursion and . The same recursion, now by induction on the length of the second list, splits a spliced sum into its first and second blocks.
Write and , and choose bijections and . Splicing the two lists gives , with for and for . The disjointness in step 1.1 makes injective and its image is , so it is an ordered basis of .
The set spans . Indeed, if lies in the image, [L4] gives coordinates with . Steps 2.1 and 1.2 split this into the -block and the -block. Applying kills the first block because every lies in , leaving as a finite linear combination of .
The list is linearly independent. Suppose . By step 1.2, lies in , so [L4] supplies with . Thus the spliced ordered basis has a vanishing linear combination whose coefficients are on the first block and on the second. Its linear independence forces every .
Linear independence makes injective. It is surjective onto by that set's definition, so it is a bijection . Together with steps 3.1 and 3.2, this says that it is an ordered basis of and that is bijective.
Step 1.1 supplies and , and step 4.1 proves all the asserted properties of their complement .
Remarks
- The construction is valid when is the zero space: then , hence , and both empty lists are the ordered bases of the zero spaces.
- No choice principle is used. Both basis selections occur inside finite-dimensional spaces and are licensed by the finite extension clause of If and is a linear subspace of , then is finite-dimensional, , and if and only if .
Depends on
The kernel and image are linear subspaces, and a linear map is injective if and only if its kernel is trivial
Kernel and image of a linear map
If and is a linear subspace of , then is finite-dimensional, , and if and only if
If has a spanning set with elements, then every linearly independent subset of is finite with at most elements; in particular has no linearly independent subset equinumerous with
Finite-dimensional vector space, and its dimension ; infinite-dimensional means having no finite basis
Linear map between vector spaces over the same field
Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis
A finite list is an ordered basis if and only if every equals for exactly one ; those scalars are the coordinates of in that ordered basis
The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity
Addition of natural numbers
The principle of mathematical induction
A subset of a finite set is finite, with , and equality holds if and only if
The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition
The cardinality of a finite set
Injection, surjection, bijection
In any vector space , , , , and forces or