ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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.

Two planes in $F^{3}$ whose sum is $F^{3}$ and whose intersection is a line, computed explicitly

Example

Let $F$ be a field (Field) and let $F^{3}$ be the vector space of functions $3 \to F$ with the pointwise operations (The vector space $F^{X}$ of all functions $X \to F$ with pointwise operations, and $F^{n}$ as the case $X = n = {0, 1, \dots, n - 1}$ ), where $3 = {0, 1, 2}$ , so an element is $x = (x_{0}, x_{1}, x_{2})$ indexed from $0$ . Let $e_{1} \in F^{3}$ have coordinates $(0_{F}, 1_{F}, 0_{F})$ and put

$U : = {x \in F^{3} : x_{2} = 0_{F}}, W : = {x \in F^{3} : x_{0} = 0_{F}} .$

Then:

$U$ and $W$ are linear subspaces of $F^{3}$ (Linear subspace of a vector space);
$U + W = F^{3}$ (The sum $U + W$ of two linear subspaces and the sum $\sum_{i < n} U_{i}$ of a finite family), a decomposition of $x$ being $x = (x_{0}, x_{1}, 0_{F}) + (0_{F}, 0_{F}, x_{2})$ ;
$U \cap W = {x \in F^{3} : x_{0} = 0_{F} and x_{2} = 0_{F}} = span {e_{1}}$ ;
the sum is not direct: it is not the case that $F^{3} = U \oplus W$ , because $U \cap W \neq {0_{V}}$ .

$U$ and $W$ are called planes and $U \cap W$ a line, informally and by analogy only; dimension is not available at this point in the library and nothing below uses it.

Facts & Assumptions

Given: A field $F$ , the vector space $F^{3}$ with pointwise operations, the vector $e_{1}$ , and the sets $U$ and $W$ as displayed.

[L1]

$F^{3}$ is the vector space of functions $3 \to F$ with $(x + y)_{i} = x_{i} + y_{i}$ and $(λ x)_{i} = λ x_{i}$ , where $3 = {0, 1, 2}$ ; its zero vector has all three coordinates $0_{F}$ ; and two elements are equal exactly when all three coordinates agree (The vector space $F^{X}$ of all functions $X \to F$ with pointwise operations, and $F^{n}$ as the case $X = n = {0, 1, \dots, n - 1}$ , Vector space over a field, The natural numbers $N$ (von Neumann), On $N$ the order is membership: $m < n ⟺ m \in n$ ).

[L2]

One-step test: a nonempty $T \subseteq V$ with $λ u + v \in T$ for all $λ \in F$ and $u, v \in T$ is a linear subspace (One-step subspace test: a nonempty $W \subseteq V$ is a linear subspace if and only if $λ u + v \in W$ for all $λ \in F$ and $u, v \in W$ , Linear subspace of a vector space).

[L3]

The intersection of a nonempty family of linear subspaces is a linear subspace (The intersection of a nonempty family of linear subspaces of $V$ is a linear subspace of $V$ ).

[L4]

$U + W = {u + w : u \in U, w \in W}$ , and it is a linear subspace (The sum $U + W$ of two linear subspaces and the sum $\sum_{i < n} U_{i}$ of a finite family).

[L5]

$span {v} = {λ v : λ \in F}$ ( $span {v} = {λ v : λ \in F}$ , which is ${0_{V}}$ when $v = 0_{V}$ , and when $v \neq 0_{V}$ contains $0_{V}$ only as the multiple $0_{F} v$ , Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ ).

[L6]

For two summands, $F^{3} = U \oplus W$ requires $U + W = F^{3}$ and $U \cap W = {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}$ ).

[L7]

In a field: $1_{F} \neq 0_{F}$ ; $λ 1_{F} = λ$ ; $0_{F} λ = 0_{F}$ (Multiplication by zero: $0 \cdot a = 0$ ) and multiplication is commutative, so $λ 0_{F} = 0_{F}$ ; and $0_{F}$ is the additive identity (Field).

Verification

technique · direct

1.1

$F^{3}$ is the set of functions $3 \to F$ with coordinatewise operations, and $e_{1}$ has coordinates $(0_{F}, 1_{F}, 0_{F})$ , so $e_{1} \in F^{3}$ .

L1L7

1.2

$U$ is a linear subspace: it contains the zero vector, whose coordinate at index $2$ is $0_{F}$ , so it is nonempty; and for $λ \in F$ and $u, v \in U$ the vector $λ u + v$ has $(λ u + v)_{2} = λ u_{2} + v_{2} = λ 0_{F} + 0_{F} = 0_{F}$ , so it lies in $U$ . The same argument at index $0$ shows $W$ is a linear subspace.

L1L2L7

1.3

$U \cap W = {x \in F^{3} : x_{0} = 0_{F} and x_{2} = 0_{F}}$ , directly from the two defining conditions.

1.4

The scalar multiples of $e_{1}$ are exactly the vectors with coordinates $(0_{F}, λ, 0_{F})$ : $(λ e_{1})_{0} = λ 0_{F} = 0_{F}$ , $(λ e_{1})_{1} = λ 1_{F} = λ$ and $(λ e_{1})_{2} = λ 0_{F} = 0_{F}$ . Conversely a vector $x$ with $x_{0} = x_{2} = 0_{F}$ agrees with $x_{1} e_{1}$ at all three indices, so $x = x_{1} e_{1}$ .

L1L7

2.1

Claim 1 is step 1.2.

step 1.2L2

2.2

Claim 3: by steps 1.3 and 1.4 the intersection $U \cap W$ is exactly ${λ e_{1} : λ \in F}$ , which is $span {e_{1}}$ ; it is a linear subspace, being an intersection of two of them.

step 1.3step 1.4L3L5

2.3

Claim 2: given $x \in F^{3}$ , put $u : = (x_{0}, x_{1}, 0_{F})$ and $w : = (0_{F}, 0_{F}, x_{2})$ . Then $u \in U$ and $w \in W$ by step 1.2, and $u + w$ has coordinates $(x_{0} + 0_{F}, x_{1} + 0_{F}, 0_{F} + x_{2}) = (x_{0}, x_{1}, x_{2})$ , so $u + w = x$ . Hence $F^{3} \subseteq U + W$ , and the reverse inclusion holds because $U + W$ is a subset of $F^{3}$ .

step 1.2L1L4L7

3.1

Claim 4: $e_{1} \in U \cap W$ by step 2.2, and $e_{1} \neq 0_{V}$ because its coordinate at index $1$ is $1_{F} \neq 0_{F}$ ; so $U \cap W \neq {0_{V}}$ and the condition for a direct sum of two summands fails.

step 2.2L1L6L7

4.1

Claims 1, 2, 3 and 4 are steps 2.1, 2.3, 2.2 and 3.1: the two planes have sum $F^{3}$ and intersection $span {e_{1}}$ , and the sum is not direct.

step 2.1step 2.2step 2.3step 3.1∎

Remarks

A sum can be everything without being direct. Condition (D1) holds here and (D2) fails, and the two are independent: the failure is exactly the nonzero overlap $span {e_{1}}$ . Concretely, $e_{1}$ decomposes in more than one way, for instance as $e_{1} + 0_{V}$ with $e_{1} \in U$ and as $0_{V} + e_{1}$ with $e_{1} \in W$ .
The intersection did not have to be computed by hand to know it is a subspace, since intersections of linear subspaces always are (The intersection of a nonempty family of linear subspaces of $V$ is a linear subspace of $V$ ). What the computation adds is the identification of that subspace as $span {e_{1}}$ , which is the point of the example.
Everything here is over an arbitrary field. No order, no square roots and no counting are used; the only field facts needed are $1_{F} \neq 0_{F}$ and the identity laws.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Linear subspace (Wikipedia) (standard reference, not scraped)
Examples of vector spaces (Wikipedia) (standard reference, not scraped)

Two planes in F3F3 whose sum is F3F3 and whose intersection is a line, computed explicitly