ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck 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 \,\}, \qquad 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 \text{ and } x_2 = 0_F \,\} = \operatorname{span}\{e_1\}$ ;
the sum is not direct: it is not the case that $F^{3} = U \oplus W$ , because $U \cap W \ne \{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 $(\lambda x)_i = \lambda 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 $\mathbb{N}$ (von Neumann), On $\mathbb{N}$ the order is membership: $m < n \iff m \in n$ ).

[L2]

One-step test: a nonempty $T \subseteq V$ with $\lambda u + v \in T$ for all $\lambda \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 $\lambda u + v \in W$ for all $\lambda \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]

$\operatorname{span}\{v\} = \{\, \lambda v : \lambda \in F \,\}$ ( $\operatorname{span}\{v\} = \{\, \lambda v : \lambda \in F \,\}$ , which is $\{0_V\}$ when $v = 0_V$ , and when $v \ne 0_V$ contains $0_V$ only as the multiple $0_F v$ , Linear combination of a finite list, and the span $\operatorname{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 = \bigoplus_{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 \ne 0_F$ ; $\lambda 1_F = \lambda$ ; $0_F \lambda = 0_F$ (Multiplication by zero: $0 \cdot a = 0$ ) and multiplication is commutative, so $\lambda 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 $\lambda \in F$ and $u, v \in U$ the vector $\lambda u + v$ has $(\lambda u + v)_2 = \lambda u_2 + v_2 = \lambda 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 \text{ 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, \lambda, 0_F)$ : $(\lambda e_1)_0 = \lambda 0_F = 0_F$ , $(\lambda e_1)_1 = \lambda 1_F = \lambda$ and $(\lambda e_1)_2 = \lambda 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 $\{\, \lambda e_1 : \lambda \in F \,\}$ , which is $\operatorname{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 \ne 0_V$ because its coordinate at index $1$ is $1_F \ne 0_F$ ; so $U \cap W \ne \{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 $\operatorname{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 $\operatorname{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 $\operatorname{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 \ne 0_F$ and the identity laws.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 56 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

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

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