Working my way through this resource on abstract algebra, and a few questions pop up from time to time.
Here is a statement regarding fields and Galois groups I find puzzling:
Proposition 23.17: Let be $E$ be a splitting field over $F$ of a separable polynomial. Then $E_{G(E/F)} = F$.
Here, $G(E/F) : = \{\sigma \in \mathrm{Aut}(E) : \sigma(\alpha) = \alpha, \; \forall \alpha \in F\}$ is the Galois group of $E$ over $F$, and $E_{G(E/F)} = \{ \alpha \in E : \sigma(\alpha) = \alpha, \; \forall \sigma \in G(E/F)\}$ is the fixed field of $E$ w.r.t $G(E/F)$.
To me, this intuitively feels like a tautology - i.e. using brackets for comprehension, it is the statement that "the sub-field of $E$ consisting of elements fixed by [the group whose members leave $F$ invariant] is $F$".
There is a short proof provided, which does not make this clear to me:
Let $G=G(E/F)$. Clearly, $F \subset E_G \subset E$. Also, $E$ must be a splitting field of $E_G$ and $G(E/F) = G(E/E_G)$. By Theorem 23.7 [which is about a splitting field $E$ for a polynomial in $F[x]$ which is separable]
$|G| = [E:E_G] = [E:F]$.
Therefore $[E_G:F]=1$. Consequently $E_G =F$.
What makes the Proposition a (relatively) non-trivial statement? The key piece seems to be that we have a splitting field whose minimal polynomial over $F$ is separable in $E$, but I can't see a way through.
(This is slightly before the fundamental theorem on Galois theory is proven, so it would be helpful to see this without using it.)