This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablfac.c ⊢ 𝐶 = { 𝑟 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝐺 ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) }
ablfac.1 ⊢ ( 𝜑 → 𝐺 ∈ Abel )
ablfac.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
Assertion ablfac ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ablfac.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ablfac.c ⊢ 𝐶 = { 𝑟 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝐺 ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) }
3 ablfac.1 ⊢ ( 𝜑 → 𝐺 ∈ Abel )
4 ablfac.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
5 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
6 1 subgid ⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) )
7 eqid ⊢ ( od ‘ 𝐺 ) = ( od ‘ 𝐺 )
8 eqid ⊢ { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) } = { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) }
9 eqid ⊢ ( 𝑝 ∈ { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) } ↦ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) = ( 𝑝 ∈ { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) } ↦ { 𝑥 ∈ 𝐵 ∣ ( ( od ‘ 𝐺 ) ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
10 eqid ⊢ ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ↦ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) } ) = ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ↦ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) } )
11 1 2 3 4 7 8 9 10 ablfaclem1 ⊢ ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ↦ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) } ) ‘ 𝐵 ) = { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) } )
12 3 5 6 11 4syl ⊢ ( 𝜑 → ( ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ↦ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) } ) ‘ 𝐵 ) = { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) } )
13 1 2 3 4 7 8 9 10 ablfaclem3 ⊢ ( 𝜑 → ( ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ↦ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) } ) ‘ 𝐵 ) ≠ ∅ )
14 12 13 eqnetrrd ⊢ ( 𝜑 → { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) } ≠ ∅ )
15 rabn0 ⊢ ( { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) } ≠ ∅ ↔ ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) )
16 14 15 sylib ⊢ ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) )