Normality is preserved under any monotone subgroup-defining function

Statement

Suppose $f$ is a monotone subgroup-defining function, i.e., $f$ is a subgroup-defining function such that whenever $H\leq G$ are groups, $f(H)\leq f(G)$. Then, the following is true:

If $H\leq G$ and $H$ is a normal subgroup of $G$, then $f(H)$ is a normal subgroup of $f(G)$.

Facts used

1. Subgroup-defining function value is characteristic
2. Characteristic of normal implies normal
3. Normality satisfies intermediate subgroup condition

Proof

Given: $H$ is a normal subgroup of $G$, $f$ is a monotone subgroup-defining function.

To prove: $f(H)$ is a normal subgroup of $f(G)$.

Proof:

Step no.	Assertion/construction	Facts used	Given data used	Previous steps used	Explanation
1	$f(H)$ is a characteristic subgroup of $H$.	Fact (1)	$f$ is a subgroup-defining function.		Given-fact-combination direct
2	$f(H)$ is a normal subgroup of $G$.	Fact (2)	$H$ is a normal subgroup of $G$.	Step (1)	Given-fact-step-combination direct
3	$f(H)$ is a subgroup of $f(G)$. In other words, $f(G)$ is an intermediate subgroup between $f(H)$ and $G$.		$f$ is monotone, $H\leq G$		given-direct
4	$f(H)$ is a normal subgroup of $f(G)$.			Steps (2), (3)	Step-combination direct