[proofplan]
We verify the group axioms for the subset $k^\times$ using only the field axioms. The only point requiring proof beyond restriction of the field operations is closure: the product of two nonzero field elements is nonzero. Once closure is established, associativity, commutativity, the identity element, and inverses follow from the corresponding field axioms, with one final check that each inverse remains nonzero.
[/proofplan]
[step:Show that $1_k$ belongs to $k^\times$]
By the field axiom $0_k \neq 1_k$. Since $k^\times$ is defined as $k \setminus \{0_k\}$, it follows that $1_k \in k^\times$.
[/step]
[step:Prove that multiplication is closed on $k^\times$]
Let $a,b \in k^\times$. Thus $a \neq 0_k$ and $b \neq 0_k$. By the field axioms, there exist elements $a^{-1}, b^{-1} \in k$ such that
\begin{align*}
a^{-1}a = 1_k \quad \text{and} \quad bb^{-1} = 1_k.
\end{align*}
We prove that $ab \neq 0_k$. Suppose, for contradiction, that $ab = 0_k$. Multiplying this equality on the left by $a^{-1}$ and on the right by $b^{-1}$, and using associativity of multiplication in $k$, gives
\begin{align*}
a^{-1}(ab)b^{-1} = a^{-1}0_k b^{-1}.
\end{align*}
The left-hand side satisfies
\begin{align*}
a^{-1}(ab)b^{-1} = (a^{-1}a)(bb^{-1}) = 1_k 1_k = 1_k.
\end{align*}
The right-hand side is $0_k$, because $0_k$ is absorbing for multiplication in a field. Hence $1_k = 0_k$, contradicting the field axiom $0_k \neq 1_k$. Therefore $ab \neq 0_k$, so $ab \in k^\times$.
Thus the restricted multiplication map
\begin{align*}
m: k^\times \times k^\times \to k^\times, \quad (a,b) \mapsto ab
\end{align*}
is well-defined.
[guided]
We need to show that the product operation inherited from $k$ really has codomain $k^\times$. In other words, if $a$ and $b$ are nonzero elements of the field, then their product must also be nonzero.
Let $a,b \in k^\times$. By definition of $k^\times$, this means $a \neq 0_k$ and $b \neq 0_k$. Since $k$ is a field, every nonzero element has a multiplicative inverse, so there exist elements $a^{-1}, b^{-1} \in k$ satisfying
\begin{align*}
a^{-1}a = 1_k \quad \text{and} \quad bb^{-1} = 1_k.
\end{align*}
Assume for contradiction that $ab = 0_k$. The purpose of multiplying by the inverses is to cancel both factors of the product $ab$. Multiplying the equality $ab = 0_k$ on the left by $a^{-1}$ and on the right by $b^{-1}$ gives
\begin{align*}
a^{-1}(ab)b^{-1} = a^{-1}0_k b^{-1}.
\end{align*}
By associativity of multiplication in the field, the left-hand side can be regrouped as
\begin{align*}
a^{-1}(ab)b^{-1} = (a^{-1}a)(bb^{-1}).
\end{align*}
Using the defining properties of $a^{-1}$ and $b^{-1}$, this becomes
\begin{align*}
(a^{-1}a)(bb^{-1}) = 1_k1_k = 1_k.
\end{align*}
On the other hand, $0_k$ is absorbing for multiplication in a field, so
\begin{align*}
a^{-1}0_k b^{-1} = 0_k.
\end{align*}
Therefore the assumption $ab = 0_k$ forces $1_k = 0_k$, contradicting the field axiom $0_k \neq 1_k$. Hence $ab \neq 0_k$, so $ab \in k^\times$.
This proves that multiplication restricts to a map
\begin{align*}
m: k^\times \times k^\times \to k^\times, \quad (a,b) \mapsto ab.
\end{align*}
[/guided]
[/step]
[step:Restrict associativity and commutativity from the field]
Let $a,b,c \in k^\times$. Since multiplication in the field $k$ is associative,
\begin{align*}
(ab)c = a(bc).
\end{align*}
By the closure already proved, both $ab$ and $bc$ lie in $k^\times$, so this is precisely associativity for the restricted operation on $k^\times$.
Likewise, since multiplication in the field $k$ is commutative, for all $a,b \in k^\times$ we have
\begin{align*}
ab = ba.
\end{align*}
Thus the restricted multiplication on $k^\times$ is commutative.
[/step]
[step:Verify that $1_k$ is the identity element for the restricted operation]
Let $a \in k^\times$. Since $1_k \in k^\times$ and $1_k$ is the multiplicative identity of the field $k$, we have
\begin{align*}
1_k a = a \quad \text{and} \quad a1_k = a.
\end{align*}
Therefore $1_k$ is the identity element of $k^\times$ under the restricted multiplication.
[/step]
[step:Verify that every element of $k^\times$ has inverse $a^{-1}$ in $k^\times$]
Let $a \in k^\times$. Since $a \neq 0_k$ and $k$ is a field, there exists $a^{-1} \in k$ such that
\begin{align*}
aa^{-1} = 1_k \quad \text{and} \quad a^{-1}a = 1_k.
\end{align*}
It remains to check that $a^{-1} \in k^\times$. Suppose, for contradiction, that $a^{-1} = 0_k$. Then
\begin{align*}
1_k = aa^{-1} = a0_k = 0_k,
\end{align*}
contradicting $0_k \neq 1_k$. Hence $a^{-1} \neq 0_k$, so $a^{-1} \in k^\times$.
Thus every $a \in k^\times$ has inverse $a^{-1}$ inside $k^\times$.
[/step]
[step:Conclude that $k^\times$ is an abelian group]
The set $k^\times$ is closed under the restricted multiplication, the operation is associative, $1_k \in k^\times$ is an identity element, every $a \in k^\times$ has inverse $a^{-1} \in k^\times$, and the operation is commutative. Therefore $k^\times$ is an abelian group under multiplication, with identity $1_k$ and inverse operation $a \mapsto a^{-1}$.
[/step]
