TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The image of a group homomorphism is a subgroup and its kernel is a normal subgroup

Statement

The image of a group homomorphism is a subgroup and its kernel is a normal subgroup.

For every group homomorphism $f : G \to H$ , one has $im f \leq H$ and $\ker f ⊴ G$ .

Facts & Assumptions

Given: A group homomorphism $f : G \to H$ .

[L1]

The kernel is the inverse image of $e_{H}$ and the image is the set of values of $f$ (The kernel and image of a group homomorphism).

[L2]

A group homomorphism preserves products and inverses (A group homomorphism automatically satisfies $f (e) = e^{'}$ and $f (g^{- 1}) = f (g)^{- 1}$ , and $f (g^{n}) = f (g)^{n}$ for every $n \in Z$ ; for monoid homomorphisms preservation of the identity must be assumed).

[L3]

A nonempty subset closed under $x y^{- 1}$ is a subgroup (One-step subgroup test: a nonempty $H \subseteq G$ is a subgroup iff $g h^{- 1} \in H$ for all $g, h \in H$ ; the identity and the inverses of $H$ are then those of $G$ ).

[L4]

A subgroup $N$ is normal when $g N g^{- 1} = N$ for every $g \in G$ (Normal subgroup: invariance under conjugation).

Proof

technique · direct

1.1L1L2L3L4givenalgebra

The image contains $e_{H} = f (e_{G})$ and, for $f (x), f (y) \in im f$ , contains $f (x) f (y)^{- 1} = f (x y^{- 1})$ ; thus [L3] gives $im f \leq H$ .

2.1step 1.1L1L2L3L4givenalgebra

The kernel is a subgroup by the same calculation, and for $k \in \ker f$ one has $f (g k g^{- 1}) = f (g) e_{H} f (g)^{- 1} = e_{H}$ , so $g (\ker f) g^{- 1} \subseteq \ker f$ ; applying this to $g^{- 1}$ gives equality.

3.1step 1.1step 2.1∎

The conjugation calculation in step 2.1 completes both assertions.

Depends on

Dependency tree · 2 levels

Sources

Ernst, An Inquiry-Based Approach to Abstract Algebra, Homomorphisms