Is manipulating a trivial equality a logically valid proof of a formula? 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.
 A: 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}.
$$
A: 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).
A: 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.
