Lambda calculus : what about the bound variables in substituting expression?

Question

I found the following set of lemma in my lambda calculus textbook :

Lemma 1.16 Let $x, y, v$ be distinct (the usual notation convention), and let no variable bound in $M$ be free in $vPQ$. Then

(a) $[P/v][v/x]M \equiv [P/x]M$ if $v \notin \mathrm{FV}(M)$;

(b) $[x/v][v/x]M \equiv M$ if $v \notin \mathrm{FV}(M)$;

(c) $[P/x][Q/y]M \equiv [([P/x]Q)/y][P/x]M$ if $y \notin \mathrm{FV}(P)$;

(d) $[P/x][Q/y]M \equiv [Q/y][P/x]M$ if $y \notin \mathrm{FV}(P), x \notin \mathrm{FV}(Q)$;

(e) $[P/x][Q/x]M \equiv [([P/x]Q)/x]M$.

In the first lemma , the first stage of substitution can be done because $x$ is a free variable in $M$ and and no variable bound in $M$ is free in $V$. But what about variables which are free in $M$ but bound in $V$? In that case, the substitution would carry the risk of changing the semantics, like if there were a free variable in $V$, let's say $K$, and there were a term in $M$ like $\lambda.k$ then it would definitely make $K$ a bound variable in $M$ if the $X$ being replaced is at a position right to the $ \lambda .k$ and the substitution will be wrong.

How is this resolved? I am unable to see through this clearly.

Answer 1

$x$, $y$, and $v$ are variables not (arbitrary) terms. To the extent that it makes sense to say so, the only variable free in $v$ is $v$. There could still be an issue with, say, $M = \lambda v.x$, i.e. $[v/x]\lambda v.x$, but, by assumption, $v$ is not bound in $M$, so this is not a valid case; $v$ is clearly free in $vPQ$.