Is manipulating a trivial equality a logically valid proof of a formula?

Question

I was working on a proof that $r^{n/2}$ commutes with $f$ in $D_4$. I did not know where to start, so I decided to manipulate a true statement into the formula I was trying to prove, as a sort of derivation.

$$\begin{align} ef &= ef \\ r^nf &= r^0f \\ r^{n/2} r^{n/2} f &= r^{n/2} r^{-n/2} f \\ r^{n/2} f &= r^{-n/2} f \\ r^{n/2} f &= f r^{n/2} \\ \end{align} $$

However, I started second-guessing myself because I realized “$ef=ef$” is true always, regardless of whether “$r^{n/2}$ commutes with $f$” is true. This leads me wondering whether “$ef=ef \implies r^{n/2} f = f r^{n/2}$” is tautological and if, in general, if any implication beginning with a trivial equality is tautological.

Answer 1

An implication $\top \Rightarrow P$ is equivalent to $P$ itself, so proving $\top\Rightarrow P$ does indeed prove $P$. (Here $\top$ denotes a proposition that is always true.)

However, after finding a proof this way, it is very common to rewrite it as a chain of equalities by reading your chain of implication on the LHS from bottom to top and then RHS from top to bottom: $$\begin{align} r^{n/2} f &= r^{-n/2} (r^n f)\\ & = r^{-n/2} (ef) \\ &= r^{-n/2} (r^0 f )\\ & = r^{-n/2} (r^{n/2} r^{-n/2}f)\\ & = r^{-n/2}f \\ &= fr^{n/2}. \end{align} $$ This chain then may be simplified a bit: $$ r^{n/2} f = r^{-n/2} r^n f = r^{-n/2} ef = r^{-n/2}f = fr^{n/2}. $$

Answer 2

Yes, this technique is valid. It doesn't matter that $ef=ef$ is always true, since your list of equations works because it is assumed that each equation follows from the one above (and not necessarily vice versa).

Answer 3

Actually, $D_4=\langle r,s\mid r^4=e, s^2=e,srs^{-1}=e\rangle$, Then we have $$ sr^2s^{-1}=r^{-2}=r^2, $$ so $r^2$ commutes with $r$ and $s$ and hence with all elements. So it is in the center.

So you don't have to start with $ef=ef$, but it is not false.