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 
|- 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 ) )