[proofplan]
Let $C$ denote the [binary simplex code](/page/Binary%20Simplex%20Code) of dimension $3$, and let $G$ denote its generator matrix whose columns are the seven nonzero vectors of $\mathbb{F}_2^3$. A nonzero codeword in $C$ can be written as $c = aG$ for a nonzero row vector $a \in \mathbb{F}_2^3$, and its coordinates record the values of the linear functional $x \mapsto a \cdot x$ on those seven columns. Since this functional is nonzero, its kernel contains exactly four vectors, three of which are nonzero, so the functional vanishes on three coordinate positions and is nonzero on the remaining four.
[/proofplan]
[step:Rewrite a nonzero codeword as evaluations of a nonzero linear functional]
Let $c \in C$ be nonzero. By definition of $C$, there exists $a = (a_1,a_2,a_3) \in \mathbb{F}_2^3$ such that $c = aG$. Since the columns $v_1,\dots,v_7$ span $\mathbb{F}_2^3$, the equality $aG = 0$ would imply $a = 0$. Hence $a \neq 0$.
Define the map $\ell_a: \mathbb{F}_2^3 \to \mathbb{F}_2$ as follows: for each vector $x = (x_1,x_2,x_3) \in \mathbb{F}_2^3$, set $\ell_a(x) := a_1x_1 + a_2x_2 + a_3x_3$. This is a nonzero $\mathbb{F}_2$-[linear functional](/page/Linear%20Functional) because $a \neq 0$. For each index $j \in \{1,\dots,7\}$, the $j$-th coordinate of $c$ is
\begin{align*}
c_j = \ell_a(v_j).
\end{align*}
[guided]
Let $c \in C$ be a nonzero codeword. The definition of the code says that $c$ is obtained by multiplying the generator matrix $G$ on the left by a row vector $a \in \mathbb{F}_2^3$, so there exists $a = (a_1,a_2,a_3) \in \mathbb{F}_2^3$ with $c = aG$.
We first check that this vector $a$ is nonzero. If $a = 0$, then $aG = 0$, contradicting that $c$ is nonzero. Equivalently, because the columns of $G$ are all nonzero vectors of $\mathbb{F}_2^3$, they span $\mathbb{F}_2^3$, so the only row vector whose dot product with every column is zero is the zero row vector. Thus $a \neq 0$.
Now define the [linear functional](/page/Linear%20Functional) attached to $a$. It is the map $\ell_a: \mathbb{F}_2^3 \to \mathbb{F}_2$ defined as follows: for each vector $x = (x_1,x_2,x_3) \in \mathbb{F}_2^3$, set $\ell_a(x) := a_1x_1 + a_2x_2 + a_3x_3$. This map is $\mathbb{F}_2$-linear because addition and scalar multiplication distribute through the coordinate formula. It is nonzero because $a \neq 0$: if, for instance, $a_i = 1$, then $\ell_a(e_i) = 1$, where $e_i$ is the $i$-th standard basis vector of $\mathbb{F}_2^3$.
The reason this functional is useful is that multiplying by $G$ evaluates $\ell_a$ on the columns of $G$. Since the $j$-th column of $G$ is $v_j$, the $j$-th coordinate of $c = aG$ is
\begin{align*}
c_j = a \cdot v_j = \ell_a(v_j)
\end{align*}
for every $j \in \{1,\dots,7\}$.
[/guided]
[/step]
[step:Count the nonzero vectors in the kernel of the functional]
Let
\begin{align*}
K := \ker(\ell_a) = \{x \in \mathbb{F}_2^3 : \ell_a(x) = 0\}.
\end{align*}
Choose an index $i \in \{1,2,3\}$ such that $a_i = 1$, and define $I := \{1,2,3\} \setminus \{i\}$. For each pair $(y_r)_{r \in I} \in \mathbb{F}_2^I$, there is a unique vector $x = (x_1,x_2,x_3) \in K$ with $x_r = y_r$ for all $r \in I$, namely the vector whose remaining coordinate is
\begin{align*}
x_i = \sum_{r \in I} a_r y_r.
\end{align*}
Indeed, because arithmetic is in $\mathbb{F}_2$, this choice gives
\begin{align*}
\ell_a(x) = a_i x_i + \sum_{r \in I} a_r x_r = \sum_{r \in I} a_r y_r + \sum_{r \in I} a_r y_r = 0.
\end{align*}
Conversely, if $x \in K$, then the same equation $a_i x_i + \sum_{r \in I} a_r x_r = 0$ and the identity $a_i = 1$ force $x_i = \sum_{r \in I} a_r x_r$. Thus the two free coordinates indexed by $I$ determine exactly one element of $K$, so $K$ has $2^2 = 4$ elements. Since $0 \in K$, exactly three elements of $K$ are nonzero.
[guided]
We need to count the vectors on which the functional $\ell_a$ vanishes. Define its kernel by
\begin{align*}
K := \ker(\ell_a) = \{x \in \mathbb{F}_2^3 : \ell_a(x) = 0\}.
\end{align*}
Because $a \neq 0$, at least one coordinate of $a$ is equal to $1$. Choose an index $i \in \{1,2,3\}$ such that $a_i = 1$, and let $I := \{1,2,3\} \setminus \{i\}$ be the set of the two remaining coordinate indices.
The equation defining the kernel is
\begin{align*}
a_i x_i + \sum_{r \in I} a_r x_r = 0.
\end{align*}
Since $a_i = 1$, this equation determines $x_i$ once the two coordinates $(x_r)_{r \in I}$ are chosen. More explicitly, for every pair $(y_r)_{r \in I} \in \mathbb{F}_2^I$, define $x = (x_1,x_2,x_3) \in \mathbb{F}_2^3$ by setting $x_r = y_r$ for $r \in I$ and
\begin{align*}
x_i = \sum_{r \in I} a_r y_r.
\end{align*}
Then, using arithmetic in $\mathbb{F}_2$, where $u + u = 0$ for every $u \in \mathbb{F}_2$, we get
\begin{align*}
\ell_a(x) = a_i x_i + \sum_{r \in I} a_r x_r = \sum_{r \in I} a_r y_r + \sum_{r \in I} a_r y_r = 0.
\end{align*}
Thus every choice of the two free coordinates produces an element of $K$.
Conversely, suppose $x \in K$. Then $\ell_a(x)=0$, so
\begin{align*}
a_i x_i + \sum_{r \in I} a_r x_r = 0.
\end{align*}
Using $a_i=1$, this forces
\begin{align*}
x_i = \sum_{r \in I} a_r x_r.
\end{align*}
Therefore an element of $K$ is uniquely determined by the two coordinates indexed by $I$. There are $2^2 = 4$ possible choices for those two coordinates, so $K$ has exactly four elements. One of them is the zero vector, and hence exactly three elements of $K$ are nonzero.
[/guided]
[/step]
[step:Translate the kernel count into Hamming weight]
The seven coordinate positions of $c$ are indexed by the seven nonzero vectors $v_1,\dots,v_7$ of $\mathbb{F}_2^3$. From the previous step, exactly three of these nonzero vectors lie in $K$, so exactly three coordinates satisfy
\begin{align*}
c_j = \ell_a(v_j) = 0.
\end{align*}
The remaining $7 - 3 = 4$ coordinates satisfy $\ell_a(v_j) \neq 0$. Since the only nonzero element of $\mathbb{F}_2$ is $1$, those four coordinates are equal to $1$. Hence the [Hamming weight](/page/Hamming%20Weight) of $c$ is
\begin{align*}
\operatorname{wt}(c) = 4.
\end{align*}
Since $c \in C$ was an arbitrary nonzero codeword, every nonzero word in the binary simplex code of dimension $3$ has weight $4$.
[guided]
We now translate the algebraic count into the coding-theoretic weight. The seven coordinates of $c$ correspond exactly to the seven nonzero vectors $v_1,\dots,v_7$ of $\mathbb{F}_2^3$, and the first step showed that each coordinate is obtained by evaluation:
\begin{align*}
c_j = \ell_a(v_j)
\end{align*}
for every $j \in \{1,\dots,7\}$.
The previous step proved that the kernel $K = \ker(\ell_a)$ contains exactly three nonzero vectors. Therefore exactly three of the seven indexing vectors $v_1,\dots,v_7$ lie in $K$. For precisely those three indices, the corresponding coordinate vanishes:
\begin{align*}
c_j = \ell_a(v_j) = 0.
\end{align*}
For the remaining $7 - 3 = 4$ indices, the vector $v_j$ is not in $K$, so $\ell_a(v_j) \neq 0$. The field $\mathbb{F}_2$ has exactly one nonzero element, namely $1$, so those four nonzero coordinates are all equal to $1$.
The [Hamming weight](/page/Hamming%20Weight) $\operatorname{wt}(c)$ counts the number of nonzero coordinates of $c$. We have found exactly four such coordinates, hence
\begin{align*}
\operatorname{wt}(c) = 4.
\end{align*}
Because $c \in C$ was an arbitrary nonzero codeword, every nonzero word in the binary simplex code of dimension $3$ has weight $4$.
[/guided]
[/step]
