Definition of absolute value:
$\forall x \in \mathbb{R}, (x \geq 0 \Longrightarrow |x| = x) \wedge (x < 0 \Longrightarrow |x| = -x)$
I want to use this definition in one of my proofs. So I instantiate it below.
Let $x \in \mathbb{R}.$ Let us assume $x \geq 0$.
Since $x \geq 0 \Longrightarrow |x| = x$, we can conclude that $|x| = x$ directly, by modus ponendo ponens.
I believe the above statements are correct. But is the following line also correct?
Since $x < 0 \Longrightarrow |x| = -x$, we can also conclude that $|x| = -x$, as the implication is vacuously true.
If so, is the justification rigorous enough? Is there a logical name for this derivation (analogous to modus ponendo ponens)?
I am not exactly sure what your question is here, but hopefully this will help:
If $x \geq 0$, then given (one part of) the definition, you can then indeed infer $|x| = x$, by Modus Ponens
And yes, given that $x \geq 0$, it is indeed (vacuously) true that $x < 0 \to |x| = -x$ ... but of course you already could have gotten that from your very definition.
What does not follow, however, is that $|x| = -x$. That is, just because $x < 0 \to |x| = -x$ is true does not mean that $|x| = -x$ is true.