Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-03
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.

G×HG\times H is a group with identity (eG,eH)(e_G,e_H), coordinatewise inverses, and homomorphic coordinate projections

Statement

For groups GG and HH, the componentwise operation of The external direct product G×HG\times H with componentwise multiplication makes G×HG\times H a group. Its identity is (eG,eH)(e_G,e_H), and

(g,h)−1=(g−1,h−1).(g,h)^{-1}=(g^{-1},h^{-1}).

Moreover the coordinate maps πG(g,h)=g\pi_G(g,h)=g and πH(g,h)=h\pi_H(g,h)=h are group homomorphisms.

Facts & Assumptions

Given: Groups G,HG,H with identities eG,eHe_G,e_H.

[L1]

G×HG\times H has the componentwise operation (g,h)(g′,h′)=(gg′,hh′)(g,h)(g',h')=(gg',hh') (The external direct product G×HG\times H with componentwise multiplication).

[L2]

A group operation is associative, has a two-sided identity, and gives every element a two-sided inverse (Group and abelian group).

[L3]

A map between groups is a group homomorphism exactly when it preserves products (Monoid homomorphism and group homomorphism).

Proof

technique · direct
1.1

For (g,h),(g′,h′),(g′′,h′′)∈G×H(g,h),(g',h'),(g'',h'')\in G\times H, associativity in each factor gives ((g,h)(g′,h′))(g′′,h′′)=(gg′g′′,hh′h′′)=(g,h)((g′,h′)(g′′,h′′))((g,h)(g',h'))(g'',h'')=(gg'g'',hh'h'')=(g,h)((g',h')(g'',h'')); thus the componentwise operation is associative.

L1L2givenalgebra
1.2

For every (g,h)∈G×H(g,h)\in G\times H, (eG,eH)(g,h)=(g,h)=(g,h)(eG,eH)(e_G,e_H)(g,h)=(g,h)=(g,h)(e_G,e_H); thus (eG,eH)(e_G,e_H) is a two-sided identity.

L1L2givenalgebra
1.3

For every (g,h)∈G×H(g,h)\in G\times H, (g,h)(g−1,h−1)=(eG,eH)=(g−1,h−1)(g,h)(g,h)(g^{-1},h^{-1})=(e_G,e_H)=(g^{-1},h^{-1})(g,h); so (g−1,h−1)(g^{-1},h^{-1}) is its inverse.

L1L2givenalgebra
2.1

Steps 1.1–1.3 verify the group axioms for G×HG\times H.

step 1.1step 1.2step 1.3L2
3.1

For pairs (g,h),(g′,h′)(g,h),(g',h'), πG((g,h)(g′,h′))=gg′=πG(g,h)πG(g′,h′)\pi_G((g,h)(g',h'))=gg'=\pi_G(g,h)\pi_G(g',h'); the same coordinatewise calculation holds for πH\pi_H, so both projections are homomorphisms from the group in step 2.1.

step 2.1L1L3givenalgebra
4.1

The stated identity, inverse formula, and coordinate homomorphisms follow.

step 2.1step 3.1∎

Depends on

Used by

Cited to discharge well-definedness by The external direct product G× H with componentwise multiplication.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 11 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