Systems of linear equations: Why does no one plug back in? When someone wants to solve a system of linear equations like
$$\begin{cases} 2x+y=0 \\ 3x+y=4 \end{cases}\,,$$
they might use this logic: 
$$\begin{align}
\begin{cases} 2x+y=0 \\ 3x+y=4 \end{cases} 
\iff &\begin{cases} -2x-y=0 \\ 3x+y=4 \end{cases} 
\\ 
\color{maroon}{\implies} &\begin{cases} -2x-y=0\\ x=4 \end{cases} 
\iff \begin{cases} -2(4)-y=0\\ x=4 \end{cases} 
\iff \begin{cases} y=-8\\ x=4 \end{cases}
\,.\end{align}$$
Then they conclude that $(x, y) = (4, -8)$ is a solution to the system. This turns out to be correct, but the logic seems flawed to me. As I see it, all this proves is that 
$$
  \forall{x,y\in\mathbb{R}}\quad
  \bigg(
  \begin{cases} 2x+y=0 \\ 3x+y=4 \end{cases} 
  \color{maroon}{\implies}
  \begin{cases} y=-8\\ x=4 \end{cases}
  \bigg)\,.
$$
But this statement leaves the possibility open that there is no pair $(x, y)$ in $\mathbb{R}^2$ that satisfies the system of equations.
$$ 
\text{What if}\; 
\begin{cases} 2x+y=0 \\ 3x+y=4 \end{cases} 
\;\text{has no solution?}
$$
It seems to me that to really be sure we've solved the equation, we have to plug back in for $x$ and $y$. I'm not talking about checking our work for simple mistakes. This seems like a matter of logical necessity. But of course, most people don't bother to plug back in, and it never seems to backfire on them. So why does no one plug back in?
P.S. It would be great if I could understand this for systems of two variables, but I would be deeply thrilled to understand it for systems of $n$ variables. I'm starting to use Gaussian elimination on big systems in my linear algebra class, where intuition is weaker and calculations are more complex, and still no one feels the need to plug back in.
 A: You wrote this step as an implication: 

$$\begin{cases} -2x-y=0 \\ 3x+y=4 \end{cases} \implies \begin{cases} -2x-y=0\\ x=4 \end{cases}$$

But it is in fact an equivalence:
$$\begin{cases} -2x-y=0 \\ 3x+y=4 \end{cases} \iff \begin{cases} -2x-y=0\\ x=4 \end{cases}$$
Then you have equivalences end-to-end and, as long as all steps are equivalences, you proved that the initial equations are equivalent to the end solutions, so you don't need to "plug back" and verify. Of course, carefulness is required to ensure that every step is in fact reversible.
A: All of the elementary/college textbooks I've seen do recommend checking solutions at the end by substitution. However, it's not strictly necessary because (as other answers point out) all of the steps involved are logical equivalences. 
You should be aware of what the algebra looks like, for a system of two equations in two variables, when you're not in the situation of having exactly one solution to the system (i.e., an independent system). In these cases, when you add the equations together (your second step), both variables will be eliminated. In the case of a dependent system (infinite solutions), you will get an identity, e.g., 0 = 0. In the case of an inconsistent system (no solutions), you get a contradiction, e.g., 0 = 1. 
For examples of this, consider OpenStax College Algebra Section 7.1. 
A: Another point of view.  Gaussian elimination of a system of linear equations is equivalent to multiplication by certain types of elementary matrices.  To avoid getting bogged down I will give specific examples and get you to look up more general cases if you find it of interest.
There are three basic types of row operation.

Add a multiple of an equation to another equation, say, $3$ times equation 1 to equation 2.  For example
  $$\eqalign{x+2y&=3\cr4x-5y&=6\cr}\quad\longrightarrow\quad
  \eqalign{x+2y&=3\cr7x+\phantom{1}y&=15\cr}$$
  This corresponds to multiplying the (augmented) coefficient by a certain matrix,
  $$\pmatrix{1&2&3\cr4&-5&6\cr}\quad\longrightarrow\quad
  \pmatrix{1&0\cr3&1\cr}\pmatrix{1&2&3\cr4&-5&6\cr}
  =\pmatrix{1&2&3\cr7&1&15\cr}$$
  
  Multiply an equation by a non-zero constant, say, the first row by $-2$.  For example,
  $$\eqalign{x+2y&=3\cr4x-5y&=6\cr}\quad\longrightarrow\quad
  \eqalign{-2x-4y&=-6\cr4x-5y&=6\cr}$$
  corresponds to
  $$\pmatrix{1&2&3\cr4&-5&6\cr}\quad\longrightarrow\quad
  \pmatrix{-2&0\cr0&1\cr}\pmatrix{1&2&3\cr4&-5&6\cr}
  =\pmatrix{-2&-4&-6\cr4&-5&6\cr}$$
  
  Finally, interchange two equations:
  $$\eqalign{x+2y&=3\cr4x-5y&=6\cr}\quad\longrightarrow\quad
  \eqalign{4x-5y&=6\cr x+2y&=3\cr}$$
  which corresponds to
  $$\pmatrix{1&2&3\cr4&-5&6\cr}\quad\longrightarrow\quad
  \pmatrix{0&1\cr1&0\cr}\pmatrix{1&2&3\cr4&-5&6\cr}
  =\pmatrix{4&-5&6\cr1&2&3\cr}\ .$$

And now the point: all three classes of multiplying matrices are invertible, and their inverses are matrices of the same types.  This means you can automatically get from your final equations back to the original, and checking solutions is not necessary.
However, while this works for linear equations, it does not in general work for other types of equations.  Your practice of checking solutions is absolutely correct and very important - please don't stop doing it!!
A: The key is that in solving this system of equations (or with row-reduction in general), every step is reversible.  Following the steps forward, we see that if $x$ and $y$ satisfy the equations, then $x = 4$ and $y = -8$.  That is, we conclude that $(4,-8)$ is the only possible solution, assuming a solution exists. Conversely, we can follow the arrows in the other direction to find that if $x = 4$ and $y = -8$, then the equations hold.
Take a second to confirm that those $\iff$'s aren't really $\implies$'s.
Compare this to a situation where the steps aren't reversible.  For example:
$$
\sqrt{x^2 - 3} = -1 \implies x^2 -3 = 1 \iff x^2 = 4 \iff x = \pm 2
$$
You'll notice that "squaring both sides" isn't reversible, so we can't automatically deduce that $\pm 2$ solve the orginal equation (and in fact, there is no solution).
A: Elementary row operations do preserve the solution set, for elementary matrices are invertible. 
We start with equations $2x+y=0$ and $3x+y=4$, which define the two lines depicted below

Subtracting $2x+y=0$ from $3x+y=4$, we obtain $x=4$, which defines a line parallel to the $y$-axis

Subtracting $x = 4$ twice from the equation $2x+y=0$, we obtain $y=-8$, which does define a line parallel to the $x$-axis

Note that all $4$ of these lines pass through the point $(4,-8)$.
A: dxiv has already answered your question for your specific example. But if you want to know the general case, when doing Gaussian elimination you have three kinds of basic steps:


*

*Rearrange equations: Clearly reversible.

*Multiply (both sides of) an equation by a non-zero constant: Clearly reversible because of "non-zero".

*Add any multiple of one equation to another: On a little reflection it is reversible too, since the operation can be easily undone by subtracting that same multiple of the first equation from the second.
This suffices to show that every step is reversible, and hence the system of equations has exactly the same solution-set after any sequence of basic steps. In fact, this is why you can sort of 'read off' the solution from the RREF of the original augmented matrix that represents the system of equations, because each basic step corresponds to left-multiplying the augmented matrix by an elementary matrix (which is invertible).
A: It's not hard to see that there is a solution; Notice that the equations are linearly independent. We only have three cases: either the lines are on top of each other, are parallel but a constant vertical distance apart, or cross each other at some point. Linear independence let's us know we are not dealing with case $1$ and we can just as easily plug in points to check case $2$, so only case $3$ is left. We could also just solve for $y$ and remember some basic algebra.
A: In my research I work with very large systems of linear equations. On the rare occasions that I have to work out a small system of equations by hand, I absolutely plug them in to check their correctness. Mistakes by hand are easy. When I am using a computer to handle the matrices that represent these equations, I generally trust that the computer did it correctly. I have other checks on my answers other than plugging them back in.
The second part of your question was, how do we know that the solution is unique? How do we know that there aren't other correct answers? We know this because they are linear equations. Two non-parallel lines intersect at a point. A line and a parabola can intersect at a point, two points, or not at all. This isn't a formal proof, but it should give you an idea.
To generalize this to multiple dimensions, a single linear equation in n dimensions describes a sub-space with dimension n-1. For the 3-d case, this is a 2-d plane inside that 3-d space. The solution to that system is the space where every equation intersects. The intersection of 2 spaces that have dimension n-1, has dimension n-2. For our 3-d example the intersection of two planes is a line (dimension 1).
If you have n unknowns, you know that you need n equations in order to have a unique solution. This can be explained by the fact that each equation reduces the dimension of the solution set (the number of variables), by one. When the dimension of the solution set is zero, the solution set is a point. Points are a unique solution.
I hope this helps, I have a odd way of thinking about linear algebra that confuses some of my colleagues.
