Let $A \in K^{n\times n}$; $\chi_A(\alpha)=\det(\alpha I_n -A)$ for all $\alpha\in K$ I am currently reading a text on linear algebra. The lemma that appears after the definition of the characteristic polynomial of a matrix unfortunately confuses me a lot. Let $K$ be a field.

Definition: $\chi(X)=\chi_A(X)=\det(X I_n -A)$ is called the characteristic polynomial of a Matrix $A\in K^{n\times n}$.
Lemma: $\chi_A(\alpha)=\det(\alpha I_n -A)$ for all $\alpha\in K$.
Proof:
We consider the function $$\varphi:K[X]\to K,$$ which is determined by inserting $\alpha$. This means  $$\varphi(\sum_{k=0}^n a_kX^k)=\sum_{k=0}^n a_k\alpha^k.$$ Then $\varphi(f+g)=\varphi(f) + \varphi(g)$ and $\varphi(fg)=\varphi(f)\varphi(g)$ hold for all $f,g \in K[X]$. We have $$\chi_A(X)=\det(X I_n -A)=\sum_{\sigma}\operatorname{sgn}(\sigma)b_{1\sigma(1)}(X)...b_{n\sigma(n)}(X)$$ for $XI_n-A=(b_{ij}(X))_{i,j}$ with $b_{ij}(X)\in K[X]$. Hence $$\chi_A(\alpha)=\sum_{\sigma}\operatorname{sgn}(\sigma)b_{1\sigma(1)}(\alpha)...b_{n\sigma(n)}(\alpha)=\det(\alpha I_n -A).$$

I know that K [X] is a polynomial ring that contains all polynomials over K. I also know the Leibniz formula for calculating the determinant. Apart from that, I am lost.  I would be really grateful if someone could describe in detail what is happening in this proof. Why is it necessary to show this at all? Isn't it clear that elements of K can simply be used in the definition?

If you define the characteristic polynomial as a function with input $X$ and output $det(XI-A)$ then saying $\chi_A(\alpha)=det(\alpha I - A)$ is indeed just the definition of this function. However, the definition here seems to be that $\chi_A(X)$ is a formal polynomial in the formal variable $X$. Applying this map $\varphi$ is precisely what it means to evaluate a formal polynomial at $X=\alpha$. But to do so, you need to ensure that $det(XI-A)$ is actually a polynomial in $X$. This is assured by the Leibniz expansion.
