Metamath Proof Explorer

Theorem ablfac

Description: The Fundamental Theorem of (finite) Abelian Groups. Any finite abelian group is a direct product of cyclic p-groups. (Contributed by Mario Carneiro, 27-Apr-2016) (Revised by Mario Carneiro, 3-May-2016)

Ref Expression
Hypotheses ablfac.b ⊢ B = Base G
ablfac.c ⊢ C = r ∈ SubGrp ⁡ G | G ↾ 𝑠 r ∈ CycGrp ∩ ran ⁡ pGrp
ablfac.1 ⊢ φ → G ∈ Abel
ablfac.2 ⊢ φ → B ∈ Fin
Assertion ablfac ⊢ φ → ∃ s ∈ Word C G dom ⁡ DProd s ∧ G DProd s = B

Proof

Step Hyp Ref Expression
1 ablfac.b ⊢ B = Base G
2 ablfac.c ⊢ C = r ∈ SubGrp ⁡ G | G ↾ 𝑠 r ∈ CycGrp ∩ ran ⁡ pGrp
3 ablfac.1 ⊢ φ → G ∈ Abel
4 ablfac.2 ⊢ φ → B ∈ Fin
5 ablgrp ⊢ G ∈ Abel → G ∈ Grp
6 1 subgid ⊢ G ∈ Grp → B ∈ SubGrp ⁡ G
7 eqid ⊢ od ⁡ G = od ⁡ G
8 eqid ⊢ w ∈ ℙ | w ∥ B = w ∈ ℙ | w ∥ B
9 eqid ⊢ p ∈ w ∈ ℙ | w ∥ B ⟼ x ∈ B | od ⁡ G ⁡ x ∥ p p pCnt B = p ∈ w ∈ ℙ | w ∥ B ⟼ x ∈ B | od ⁡ G ⁡ x ∥ p p pCnt B
10 eqid ⊢ g ∈ SubGrp ⁡ G ⟼ s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = g = g ∈ SubGrp ⁡ G ⟼ s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = g
11 1 2 3 4 7 8 9 10 ablfaclem1 ⊢ B ∈ SubGrp ⁡ G → g ∈ SubGrp ⁡ G ⟼ s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = g ⁡ B = s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = B
12 3 5 6 11 4syl ⊢ φ → g ∈ SubGrp ⁡ G ⟼ s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = g ⁡ B = s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = B
13 1 2 3 4 7 8 9 10 ablfaclem3 ⊢ φ → g ∈ SubGrp ⁡ G ⟼ s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = g ⁡ B ≠ ∅
14 12 13 eqnetrrd ⊢ φ → s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = B ≠ ∅
15 rabn0 ⊢ s ∈ Word C | G dom ⁡ DProd s ∧ G DProd s = B ≠ ∅ ↔ ∃ s ∈ Word C G dom ⁡ DProd s ∧ G DProd s = B
16 14 15 sylib ⊢ φ → ∃ s ∈ Word C G dom ⁡ DProd s ∧ G DProd s = B