 Solution

A binary linear code of length $n$ is a vector subspace $C\subseteq {\mathbb{F}}_2^n$. The Hamming weight of a word counts its nonzero coordinates, and the code weight is $w(C)={\min }_{0\ne c\in C}\mathrm{wt}(c)$; for a linear code this equals its minimum distance. One may assign infinite minimum weight to the zero code when needed.

For length-$n$ codes with $C_2\subseteq C_1$, the bar product of binary linear codes isIt is a linear code because this map from $C_1\oplus C_2$ is linear and injective. For a nonzero codeword, if $v=0$ then $u\ne 0$ and its weight is $2\mathrm{wt}(u)\ge 2w(C_1)$. If $v\ne 0$, every nonzero coordinate of $v$ makes exactly one of the corresponding coordinates of $u,u+v$ nonzero; henceTaking the minimum givesIn fact equality holds when the codes are nonzero: minimum-weight words $(u,u)$ and $(0,v)$ attain the two candidate weights.