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 a subspace $W$ of a finite-dimensional inner product space, $V = W \oplus W^{⊥}$

Statement

If $W$ is a subspace of a finite-dimensional real or complex inner product space $V$ , then

$V = W \oplus W^{⊥} .$

Thus every $v \in V$ has unique vectors $w \in W$ and $z \in W^{⊥}$ with $v = w + z$ .

Facts & Assumptions

Given: A subspace $W$ of a finite-dimensional inner product space $V$ .

[L1]

Every subspace of a finite-dimensional space has a finite basis that can be extended to a basis of the ambient space (If $\dim_{F} V = n$ and $U$ is a linear subspace of $V$ , then $U$ is finite-dimensional, $\dim_{F} U \leq n$ , and $\dim_{F} U = n$ if and only if $U = V$ ).

[L2]

Gram–Schmidt preserves the span of every initial segment of an independent list (Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans).

[L3]

The orthogonal complement consists of vectors pairing to zero with every vector of the subspace (The orthogonal complement $W^{⊥} = {v : ⟨ v, w ⟩ = 0 for all w \in W}$ ).

[L4]

For two summands, $V = W \oplus U$ means $W + U = V$ and $W \cap U = {0_{V}}$ (Internal direct sum $V = ⨁_{i < n} U_{i}$ : the sum is everything and each summand meets the sum of the others only in $0_{V}$ ).

Proof

technique · direct

1.1

By [L1], choose a basis $(w_{0}, \dots, w_{s - 1})$ of $W$ and extend it to a basis $(w_{0}, \dots, w_{s - 1}, v_{s}, \dots, v_{n - 1})$ of $V$ . Empty initial or terminal blocks cover $W = 0$ and $W = V$ .

L1choose

2.1

Apply [L2] to this basis, obtaining an orthonormal basis $(e_{0}, \dots, e_{n - 1})$ with $W = span (e_{0}, \dots, e_{s - 1})$ . Put $U = span (e_{s}, \dots, e_{n - 1})$ . Orthonormality and [L3] give $U \subseteq W^{⊥}$ .

step 1.1L2L3

3.1

The orthonormal basis splits every vector as a sum of a vector in $W$ and a vector in $U$ , so $V = W + U \subseteq W + W^{⊥}$ . The reverse inclusion is automatic.

step 2.1

4.1

If $x \in W \cap W^{⊥}$ , then [L3] gives $⟨ x, x ⟩ = 0$ , and positive definiteness gives $x = 0$ . With step 3.1 this is exactly the pair of conditions in [L4], so $V = W \oplus W^{⊥}$ . The decomposition of each $x$ is unique: if $w + u = w^{'} + u^{'}$ with $w, w^{'} \in W$ and $u, u^{'} \in W^{⊥}$ , then $w - w^{'} = u^{'} - u$ lies in $W \cap W^{⊥} = {0_{V}}$ , so $w = w^{'}$ and $u = u^{'}$ .

step 3.1L3L4algebra∎

Depends on

Used by

In finite dimension, W^⊥⊥=W and dim W+dim W^⊥=dim V Corollary
A nondegenerate indefinite symmetric form can have W∩ W^⊥≠0 Counterexample
The orthogonal projection P_Wv is the W-component in V=W⊕ W^⊥ Definition

Dependency tree · next 3 levels

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

Sheldon Axler, Linear Algebra Done Right, 4th ed., result 6.49 (standard reference, not scraped)
Sergei Treil, Linear Algebra Done Wrong, §5.3.3 (standard reference, not scraped)

For a subspace WW of a finite-dimensional inner product space, V=W⊕W⊥V=W⊕W⊥