Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

If H≤GH\le G and N⊴GN\mathrel{\trianglelefteq}G, then HNHN is a subgroup and H∩N⊴HH\cap N\mathrel{\trianglelefteq}H

Statement

If H≤GH\le G and N⊴GN\mathrel{\trianglelefteq}G, then HNHN is a subgroup and H∩N⊴HH\cap N\mathrel{\trianglelefteq}H.

Here HN:={hn:h∈H, n∈N}HN:=\{hn:h\in H,\ n\in N\}.

Facts & Assumptions

Given: A subgroup H≤GH\le G and a normal subgroup N⊴GN\mathrel{\trianglelefteq}G.

[L1]

A nonempty subset closed under xy−1xy^{-1} is a subgroup (One-step subgroup test: a nonempty H⊆GH \subseteq G is a subgroup iff gh−1∈Hgh^{-1} \in H for all g,h∈Hg, h \in H; the identity and the inverses of HH are then those of GG).

[L2]

Normality means gNg−1=NgNg^{-1}=N for every g∈Gg\in G (Normal subgroup: invariance under conjugation).

[L3]

A subgroup is normal if its conjugates by ambient elements lie in it (Equivalent characterisations of a normal subgroup by conjugates and left and right cosets).

[L4]

(ab)−1=b−1a−1(ab)^{-1}=b^{-1}a^{-1} in a group (In a group e−1=ee^{-1} = e, (g−1)−1=g(g^{-1})^{-1} = g and (gh)−1=h−1g−1(gh)^{-1} = h^{-1}g^{-1}, the order of the last product being essential).

Proof

technique · direct
1.1

The identity lies in HNHN; for h1n1,h2n2∈HNh_1n_1,h_2n_2\in HN, put m=n1n2−1∈Nm=n_1n_2^{-1}\in N, so (h1n1)(h2n2)−1=h1mh2−1=h1h2−1(h2mh2−1)∈HN(h_1n_1)(h_2n_2)^{-1}=h_1mh_2^{-1}=h_1h_2^{-1}(h_2mh_2^{-1})\in HN.

L1L2L3L4givenalgebra
2.1

Thus [L1] gives HN≤GHN\le G; moreover for h∈Hh\in H and x∈H∩Nx\in H\cap N, both hxh−1∈Hhxh^{-1}\in H and hxh−1∈Nhxh^{-1}\in N, so it lies in H∩NH\cap N.

step 1.1L1L2L3L4givenalgebra
3.1

The conjugation closure in step 2.1 gives H∩N⊴HH\cap N\mathrel{\trianglelefteq}H.

step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 14 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources