Proving smooth algebraic varieties remain smooth after base change by any field extension from first principles

Let $X$ be a smooth algebraic variety over a field $k$, and let $K/k$ be any field extension. I want to prove that $$ X_K:=X\times_{\operatorname{Spec}k}\operatorname{Spec}K $$ is smooth over $K$.

I want to use only the following facts:

• Jacobian criterion (rational points): If $$ X=V(I)\subset\mathbb A_k^n $$ with $I=(F_1,\ldots,F_r)$ and $x\in X(k)$, let $$ J_x=\left(\frac{\partial F_i}{\partial T_j}(x)\right). $$ Then $X$ is regular at $x$ iff $$ \operatorname{rank}(J_x)=n-\dim\mathcal O_{X,x}. $$

• Flat dimension formula: If $$ f:X\to Y $$ is a morphism of locally Noetherian schemes, $x\in X$, and $y=f(x)$, then $$ \dim\mathcal O_{X_y,x}\ge \dim\mathcal O_{X,x}-\dim\mathcal O_{Y,y}, $$ with equality if $f$ is flat.

• Over a perfect field, a variety is regular if and only if it is smooth.

• $X$ is smooth over $k$ if and only if $X_{\bar k}$ is regular.

• Smooth algebraic varieties are regular

• In a Noetherian scheme, regularity is equivalent to regularity at all its closed points.

• Over an algebraically closed field, closed points are precisely rational points.

• Flat morphisms are stable under base change.

• Noetherian normalisation

• If $X$ is an irreducible algebraic variety, then for every closed point $x\in X$, $$ \dim\mathcal O_{X,x}=\dim X. $$

Please do not use the fact that smoothness is stable under base change, or smooth morphisms are stable under base change, because I am attempting to prove these using the result here. Also, please avoid the use of differentials or cotangent sheaves, etc. I'm trying to prove only using the facts above.

The main difficulties are the following. First, while I can reduce to the case where $X$ is integral and affine (as $X$ is regular), the base-changed schemes $X_{\bar k}$ and $X_{\bar K}$ need not remain integral/irreducible. Consequently, I am not sure how to link the dimension of the local ring with the global dimension. Maybe I should reduce to the case where $X_{\bar k}$ is integral and affine instead, as it is regular?

Second, under the projection $$\pi:X_{\bar K}\longrightarrow X_{\bar k},$$ the image of a closed point $y\in X_{\bar K}$ need not be a closed point of $X_{\bar k}$. The extension $\bar K/\bar k$ is any extension, so a rational point of $X_{\bar K}$ may map to a non-closed point of $X_{\bar k}$. This prevents me from directly transferring the Jacobian rank condition from closed points of $X_{\bar k}$ to those of $X_{\bar K}$.