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 𝑠 ) = 𝐵 ) )