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 e. ( SubGrp ` G ) | ( G |`s r ) e. ( CycGrp i^i ran pGrp ) }
	ablfac.1	|- ( ph -> G e. Abel )
	ablfac.2	|- ( ph -> B e. Fin )
Assertion	ablfac	|- ( ph -> E. s e. 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 e. ( SubGrp ` G ) | ( G |`s r ) e. ( CycGrp i^i ran pGrp ) }
3		ablfac.1	|- ( ph -> G e. Abel )
4		ablfac.2	|- ( ph -> B e. Fin )
5		ablgrp	|- ( G e. Abel -> G e. Grp )
6	1	subgid	|- ( G e. Grp -> B e. ( SubGrp ` G ) )
7		eqid	|- ( od ` G ) = ( od ` G )
8		eqid	|- { w e. Prime | w || ( # ` B ) } = { w e. Prime | w || ( # ` B ) }
9		eqid	|- ( p e. { w e. Prime | w || ( # ` B ) } |-> { x e. B | ( ( od ` G ) ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } ) = ( p e. { w e. Prime | w || ( # ` B ) } |-> { x e. B | ( ( od ` G ) ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )
10		eqid	|- ( g e. ( SubGrp ` G ) |-> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = g ) } ) = ( g e. ( SubGrp ` G ) |-> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = g ) } )
11	1 2 3 4 7 8 9 10	ablfaclem1	|- ( B e. ( SubGrp ` G ) -> ( ( g e. ( SubGrp ` G ) |-> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = g ) } ) ` B ) = { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = B ) } )
12	3 5 6 11	4syl	|- ( ph -> ( ( g e. ( SubGrp ` G ) |-> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = g ) } ) ` B ) = { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = B ) } )
13	1 2 3 4 7 8 9 10	ablfaclem3	|- ( ph -> ( ( g e. ( SubGrp ` G ) |-> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = g ) } ) ` B ) =/= (/) )
14	12 13	eqnetrrd	|- ( ph -> { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = B ) } =/= (/) )
15		rabn0	|- ( { s e. Word C | ( G dom DProd s /\ ( G DProd s ) = B ) } =/= (/) <-> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) )
16	14 15	sylib	|- ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) )