Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16
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.

For an endomorphism in finite dimension, preserving lengths, preserving inner products, carrying orthonormal bases to orthonormal bases, and TT=I are equivalent

Statement

For an endomorphism T of a finite-dimensional real or complex inner product space V, the following are equivalent:

  1. T preserves norms.
  2. T preserves inner products.
  3. T sends every orthonormal basis to an orthonormal basis.
  4. T sends some orthonormal basis to an orthonormal basis.
  5. TT=I.

Whenever these conditions hold, T is invertible and T1=T, so also TT=I. The zero-dimensional case is included.

Facts & Assumptions

Given: An endomorphism T of a finite-dimensional inner product space V.

[L1]

Real and complex polarisation identities recover the inner product from the norm (Pythagoras, the parallelogram identity, and the real and complex polarisation identities).

[L2]

Every finite-dimensional inner product space has an orthonormal basis (Every finite-dimensional real or complex inner product space has an orthonormal basis).

[L3]
[L5]

A linear isometry is a linear map preserving every vector norm (Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces).

[L6]

If z,w=0 for every w in an inner product space, then z=0 (Inner products separate vectors, and the induced norm is homogeneous: λv=λv).

[L7]

Every finite orthogonal list of nonzero vectors is linearly independent (Every finite orthogonal list of nonzero vectors is linearly independent).

[L8]

A subspace of a finite-dimensional space has the same dimension as the ambient space exactly when it is the whole space (If dimFV=n and U is a linear subspace of V, then U is finite-dimensional, dimFUn, and dimFU=n if and only if U=V).

Proof

technique · equivalence
1.1

If T preserves norms, substitute Tu,Tv into the appropriate real or complex polarisation identity [L1]. Every norm term is unchanged, so Tu,Tv=u,v. Thus (1) implies (2).

L1L5
1.2

If T preserves inner products, it sends every orthonormal basis to an orthonormal list. By [L7] this list is independent; its span therefore has dimension dimV, so [L8] makes it all of V. Thus (2) implies (3), while (3) implies (4) by the existence in [L2].

L2L7L8
1.3

Suppose an orthonormal basis (ei) has orthonormal image (Tei). Expanding arbitrary u,v in (ei) shows directly that Tu,Tv=u,v. Hence (4) implies (2), and setting u=v shows (2) implies (1).

L2algebra
1.4

By the defining adjoint identity [L3], (2) is equivalent to u,(TTI)v=0 for all u,v. Conjugate symmetry and nondegeneracy [L6] make this equivalent to (TTI)v=0 for every v, hence to TT=I. Thus (2) and (5) are equivalent.

L3L6algebra
1.5

Under (5), multiplicativity in [L4] gives det(T)det(T)=1, so det(T)0. Hence T is invertible and TT=I gives T1=T. Consequently TT=I.

L4
2.1

All implications remain valid for the empty orthonormal basis of V=0, where the identity endomorphism is the unique map.

L2

Depends on

Used by

Dependency tree · next 3 levels

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