A subspace and its orthogonal complement split the space

The statement asserts the following, for every choice of the data it quantifies over: let $V$ be a type carrying a normed additive commutative group structure together with a real inner product space structure $\langle\cdot,\cdot\rangle : V \times V \to \mathbb{R}$ compatible with that norm, and assume in addition that $V$ is finite-dimensional as a vector space over $\mathbb{R}$ (these three structural assumptions are hypotheses of the claim; no completeness beyond what finite-dimensionality gives is assumed separately, and $V$ is not assumed nonzero — the zero space is included); and let $S$ be an arbitrary $\mathbb{R}$-linear subspace of $V$ (an arbitrary element of the lattice of submodules, so the degenerate choices $S = \{0\}$ and $S = V$ are both included). Write

for the orthogonal complement of $S$, itself a subspace. Then the claim is that $S$ and $S^{\perp}$ are complements of each other in the lattice of subspaces of $V$, which unfolds to the conjunction of exactly two conditions:

• Disjointness: every subspace contained in both $S$ and $S^{\perp}$ is the zero subspace; equivalently $S \cap S^{\perp} = \{0\}$.
• Codisjointness: every subspace containing both $S$ and $S^{\perp}$ is all of $V$; equivalently the subspace sum satisfies $S + S^{\perp} = V$, i.e. every $v \in V$ can be written as $v = s + t$ with $s \in S$ and $t \in S^{\perp}$.

Nothing further is asserted: the statement is a bare lattice-complementation claim about the pair $(S, S^{\perp})$. In particular it does not itself name, construct, or characterize a projection map, states no uniqueness of the decomposition $v = s + t$ as a separate clause (uniqueness follows from the two conditions above but is not written), asserts no formula such as a Pythagorean identity $\|v\|^2 = \|s\|^2 + \|t\|^2$ or a dimension count $\dim S + \dim S^{\perp} = \dim V$, and says nothing about the second orthogonal complement $S^{\perp\perp}$. The two degenerate instances are covered and are asserted along with the rest: for $S = \{0\}$ the claim says $\{0\}$ and $V$ are complementary, and for $S = V$ it says $V$ and $\{0\}$ are. The hypotheses are satisfiable (e.g. $V = \mathbb{R}^n$ with the standard inner product), so the assertion is not vacuous.