Noetherianness is extension-closed

This article gives the statement, and possibly proof, of a group property (i.e., Noetherian group) satisfying a group metaproperty (i.e., extension-closed group property)
View all group metaproperty satisfactions | View all group metaproperty dissatisfactions |Get help on looking up metaproperty (dis)satisfactions for group properties
Get more facts about Noetherian group |Get facts that use property satisfaction of Noetherian group | Get facts that use property satisfaction of Noetherian group|Get more facts about extension-closed group property

Statement

Suppose $G$ is a group and $H$ is a normal subgroup of $G$. Then, if both $H$ and $G/H$ are Noetherian groups (i.e., every subgroup of either is finitely generated), then $G$ is also Noetherian.

Facts used

1. Finite generation is extension-closed
2. Second isomorphism theorem

Proof

Given: $G$ is a group, $H$ is a normal subgroup of $G$. Both $H$ and $G/H$ are Noetherian. $K$ is a subgroup of $G$.

To prove: $K$ is finitely generated.

Proof:

Step no.	Assertion/construction	Facts used	Given data used	Previous steps used	Explanation
1	$H\cap K$ is finitely generated		$H$ is Noetherian.		Fact-given direct
2	$K/(H\cap K)\cong HK/H$ and hence is isomorphic to a subgroup of $G/H$.	Fact (2)	$H,K\leq G$, $H$ normal.		Fact-given direct
3	$HK/H$ is a finitely generated group		$G/H$ is Noetherian		Given-direct
4	$K/(H\cap K)$ is finitely generated			Steps (2), (3)	Step-combination direct
5	$K$ is finitely generated	Fact (1)		Steps (1), (4)	Fact-step-combination direct