Metamath Proof Explorer

Theorem pgpfac

Description: Full factorization of a finite abelian p-group, by iterating pgpfac1 . There is a direct product decomposition of any abelian group of prime-power order into cyclic subgroups. (Contributed by Mario Carneiro, 27-Apr-2016) (Revised by Mario Carneiro, 3-May-2016)

Ref Expression
Hypotheses pgpfac.b 
|- B = ( Base ` G )
pgpfac.c 
|- C = { r e. ( SubGrp ` G ) | ( G |`s r ) e. ( CycGrp i^i ran pGrp ) }
pgpfac.g 
|- ( ph -> G e. Abel )
pgpfac.p 
|- ( ph -> P pGrp G )
pgpfac.f 
|- ( ph -> B e. Fin )
Assertion pgpfac 
|- ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) )

Proof

Step Hyp Ref Expression
1 pgpfac.b 
 |-  B = ( Base ` G )
2 pgpfac.c 
 |-  C = { r e. ( SubGrp ` G ) | ( G |`s r ) e. ( CycGrp i^i ran pGrp ) }
3 pgpfac.g 
 |-  ( ph -> G e. Abel )
4 pgpfac.p 
 |-  ( ph -> P pGrp G )
5 pgpfac.f 
 |-  ( ph -> B e. Fin )
6 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
7 1 subgid 
 |-  ( G e. Grp -> B e. ( SubGrp ` G ) )
8 3 6 7 3syl 
 |-  ( ph -> B e. ( SubGrp ` G ) )
9 eleq1 
 |-  ( t = u -> ( t e. ( SubGrp ` G ) <-> u e. ( SubGrp ` G ) ) )
10 eqeq2 
 |-  ( t = u -> ( ( G DProd s ) = t <-> ( G DProd s ) = u ) )
11 10 anbi2d 
 |-  ( t = u -> ( ( G dom DProd s /\ ( G DProd s ) = t ) <-> ( G dom DProd s /\ ( G DProd s ) = u ) ) )
12 11 rexbidv 
 |-  ( t = u -> ( E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) <-> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = u ) ) )
13 9 12 imbi12d 
 |-  ( t = u -> ( ( t e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) <-> ( u e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = u ) ) ) )
14 13 imbi2d 
 |-  ( t = u -> ( ( ph -> ( t e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) <-> ( ph -> ( u e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = u ) ) ) ) )
15 eleq1 
 |-  ( t = B -> ( t e. ( SubGrp ` G ) <-> B e. ( SubGrp ` G ) ) )
16 eqeq2 
 |-  ( t = B -> ( ( G DProd s ) = t <-> ( G DProd s ) = B ) )
17 16 anbi2d 
 |-  ( t = B -> ( ( G dom DProd s /\ ( G DProd s ) = t ) <-> ( G dom DProd s /\ ( G DProd s ) = B ) ) )
18 17 rexbidv 
 |-  ( t = B -> ( E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) <-> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) ) )
19 15 18 imbi12d 
 |-  ( t = B -> ( ( t e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) <-> ( B e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) ) ) )
20 19 imbi2d 
 |-  ( t = B -> ( ( ph -> ( t e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) <-> ( ph -> ( B e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) ) ) ) )
21 bi2.04 
 |-  ( ( t C. u -> ( t e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) <-> ( t e. ( SubGrp ` G ) -> ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) )
22 21 imbi2i 
 |-  ( ( ph -> ( t C. u -> ( t e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) ) <-> ( ph -> ( t e. ( SubGrp ` G ) -> ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) ) )
23 bi2.04 
 |-  ( ( t C. u -> ( ph -> ( t e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) ) <-> ( ph -> ( t C. u -> ( t e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) ) )
24 bi2.04 
 |-  ( ( t e. ( SubGrp ` G ) -> ( ph -> ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) ) <-> ( ph -> ( t e. ( SubGrp ` G ) -> ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) ) )
25 22 23 24 3bitr4i 
 |-  ( ( t C. u -> ( ph -> ( t e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) ) <-> ( t e. ( SubGrp ` G ) -> ( ph -> ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) ) )
26 25 albii 
 |-  ( A. t ( t C. u -> ( ph -> ( t e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) ) <-> A. t ( t e. ( SubGrp ` G ) -> ( ph -> ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) ) )
27 df-ral 
 |-  ( A. t e. ( SubGrp ` G ) ( ph -> ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) <-> A. t ( t e. ( SubGrp ` G ) -> ( ph -> ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) ) )
28 r19.21v 
 |-  ( A. t e. ( SubGrp ` G ) ( ph -> ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) <-> ( ph -> A. t e. ( SubGrp ` G ) ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) )
29 26 27 28 3bitr2i 
 |-  ( A. t ( t C. u -> ( ph -> ( t e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) ) <-> ( ph -> A. t e. ( SubGrp ` G ) ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) )
30 3 adantr 
 |-  ( ( ph /\ ( A. t e. ( SubGrp ` G ) ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) /\ u e. ( SubGrp ` G ) ) ) -> G e. Abel )
31 4 adantr 
 |-  ( ( ph /\ ( A. t e. ( SubGrp ` G ) ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) /\ u e. ( SubGrp ` G ) ) ) -> P pGrp G )
32 5 adantr 
 |-  ( ( ph /\ ( A. t e. ( SubGrp ` G ) ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) /\ u e. ( SubGrp ` G ) ) ) -> B e. Fin )
33 simprr 
 |-  ( ( ph /\ ( A. t e. ( SubGrp ` G ) ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) /\ u e. ( SubGrp ` G ) ) ) -> u e. ( SubGrp ` G ) )
34 simprl 
 |-  ( ( ph /\ ( A. t e. ( SubGrp ` G ) ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) /\ u e. ( SubGrp ` G ) ) ) -> A. t e. ( SubGrp ` G ) ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) )
35 psseq1 
 |-  ( t = x -> ( t C. u <-> x C. u ) )
36 eqeq2 
 |-  ( t = x -> ( ( G DProd s ) = t <-> ( G DProd s ) = x ) )
37 36 anbi2d 
 |-  ( t = x -> ( ( G dom DProd s /\ ( G DProd s ) = t ) <-> ( G dom DProd s /\ ( G DProd s ) = x ) ) )
38 37 rexbidv 
 |-  ( t = x -> ( E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) <-> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = x ) ) )
39 35 38 imbi12d 
 |-  ( t = x -> ( ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) <-> ( x C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = x ) ) ) )
40 39 cbvralvw 
 |-  ( A. t e. ( SubGrp ` G ) ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) <-> A. x e. ( SubGrp ` G ) ( x C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = x ) ) )
41 34 40 sylib 
 |-  ( ( ph /\ ( A. t e. ( SubGrp ` G ) ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) /\ u e. ( SubGrp ` G ) ) ) -> A. x e. ( SubGrp ` G ) ( x C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = x ) ) )
42 1 2 30 31 32 33 41 pgpfaclem3 
 |-  ( ( ph /\ ( A. t e. ( SubGrp ` G ) ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) /\ u e. ( SubGrp ` G ) ) ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = u ) )
43 42 exp32 
 |-  ( ph -> ( A. t e. ( SubGrp ` G ) ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) -> ( u e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = u ) ) ) )
44 43 a1i 
 |-  ( u e. Fin -> ( ph -> ( A. t e. ( SubGrp ` G ) ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) -> ( u e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = u ) ) ) ) )
45 44 a2d 
 |-  ( u e. Fin -> ( ( ph -> A. t e. ( SubGrp ` G ) ( t C. u -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) -> ( ph -> ( u e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = u ) ) ) ) )
46 29 45 syl5bi 
 |-  ( u e. Fin -> ( A. t ( t C. u -> ( ph -> ( t e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) ) ) -> ( ph -> ( u e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = u ) ) ) ) )
47 14 20 46 findcard3 
 |-  ( B e. Fin -> ( ph -> ( B e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) ) ) )
48 5 47 mpcom 
 |-  ( ph -> ( B e. ( SubGrp ` G ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) ) )
49 8 48 mpd 
 |-  ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) )