Metamath Proof Explorer

Theorem pgpfac1

Description: Factorization of a finite abelian p-group. There is a direct product decomposition of any abelian group of prime-power order where one of the factors is cyclic and generated by an element of maximal order. (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypotheses pgpfac1.k 
|- K = ( mrCls ` ( SubGrp ` G ) )
pgpfac1.s 
|- S = ( K ` { A } )
pgpfac1.b 
|- B = ( Base ` G )
pgpfac1.o 
|- O = ( od ` G )
pgpfac1.e 
|- E = ( gEx ` G )
pgpfac1.z 
|- .0. = ( 0g ` G )
pgpfac1.l 
|- .(+) = ( LSSum ` G )
pgpfac1.p 
|- ( ph -> P pGrp G )
pgpfac1.g 
|- ( ph -> G e. Abel )
pgpfac1.n 
|- ( ph -> B e. Fin )
pgpfac1.oe 
|- ( ph -> ( O ` A ) = E )
pgpfac1.ab 
|- ( ph -> A e. B )
Assertion pgpfac1 
|- ( ph -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = B ) )

Proof

Step Hyp Ref Expression
1 pgpfac1.k 
 |-  K = ( mrCls ` ( SubGrp ` G ) )
2 pgpfac1.s 
 |-  S = ( K ` { A } )
3 pgpfac1.b 
 |-  B = ( Base ` G )
4 pgpfac1.o 
 |-  O = ( od ` G )
5 pgpfac1.e 
 |-  E = ( gEx ` G )
6 pgpfac1.z 
 |-  .0. = ( 0g ` G )
7 pgpfac1.l 
 |-  .(+) = ( LSSum ` G )
8 pgpfac1.p 
 |-  ( ph -> P pGrp G )
9 pgpfac1.g 
 |-  ( ph -> G e. Abel )
10 pgpfac1.n 
 |-  ( ph -> B e. Fin )
11 pgpfac1.oe 
 |-  ( ph -> ( O ` A ) = E )
12 pgpfac1.ab 
 |-  ( ph -> A e. B )
13 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
14 3 subgid 
 |-  ( G e. Grp -> B e. ( SubGrp ` G ) )
15 9 13 14 3syl 
 |-  ( ph -> B e. ( SubGrp ` G ) )
16 eleq1 
 |-  ( s = u -> ( s e. ( SubGrp ` G ) <-> u e. ( SubGrp ` G ) ) )
17 eleq2 
 |-  ( s = u -> ( A e. s <-> A e. u ) )
18 16 17 anbi12d 
 |-  ( s = u -> ( ( s e. ( SubGrp ` G ) /\ A e. s ) <-> ( u e. ( SubGrp ` G ) /\ A e. u ) ) )
19 eqeq2 
 |-  ( s = u -> ( ( S .(+) t ) = s <-> ( S .(+) t ) = u ) )
20 19 anbi2d 
 |-  ( s = u -> ( ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) <-> ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = u ) ) )
21 20 rexbidv 
 |-  ( s = u -> ( E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) <-> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = u ) ) )
22 18 21 imbi12d 
 |-  ( s = u -> ( ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) <-> ( ( u e. ( SubGrp ` G ) /\ A e. u ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = u ) ) ) )
23 22 imbi2d 
 |-  ( s = u -> ( ( ph -> ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) <-> ( ph -> ( ( u e. ( SubGrp ` G ) /\ A e. u ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = u ) ) ) ) )
24 eleq1 
 |-  ( s = B -> ( s e. ( SubGrp ` G ) <-> B e. ( SubGrp ` G ) ) )
25 eleq2 
 |-  ( s = B -> ( A e. s <-> A e. B ) )
26 24 25 anbi12d 
 |-  ( s = B -> ( ( s e. ( SubGrp ` G ) /\ A e. s ) <-> ( B e. ( SubGrp ` G ) /\ A e. B ) ) )
27 eqeq2 
 |-  ( s = B -> ( ( S .(+) t ) = s <-> ( S .(+) t ) = B ) )
28 27 anbi2d 
 |-  ( s = B -> ( ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) <-> ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = B ) ) )
29 28 rexbidv 
 |-  ( s = B -> ( E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) <-> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = B ) ) )
30 26 29 imbi12d 
 |-  ( s = B -> ( ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) <-> ( ( B e. ( SubGrp ` G ) /\ A e. B ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = B ) ) ) )
31 30 imbi2d 
 |-  ( s = B -> ( ( ph -> ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) <-> ( ph -> ( ( B e. ( SubGrp ` G ) /\ A e. B ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = B ) ) ) ) )
32 bi2.04 
 |-  ( ( s C. u -> ( s e. ( SubGrp ` G ) -> ( A e. s -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) <-> ( s e. ( SubGrp ` G ) -> ( s C. u -> ( A e. s -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) )
33 impexp 
 |-  ( ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) <-> ( s e. ( SubGrp ` G ) -> ( A e. s -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) )
34 33 imbi2i 
 |-  ( ( s C. u -> ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) <-> ( s C. u -> ( s e. ( SubGrp ` G ) -> ( A e. s -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) )
35 impexp 
 |-  ( ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) <-> ( s C. u -> ( A e. s -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) )
36 35 imbi2i 
 |-  ( ( s e. ( SubGrp ` G ) -> ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) <-> ( s e. ( SubGrp ` G ) -> ( s C. u -> ( A e. s -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) )
37 32 34 36 3bitr4i 
 |-  ( ( s C. u -> ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) <-> ( s e. ( SubGrp ` G ) -> ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) )
38 37 imbi2i 
 |-  ( ( ph -> ( s C. u -> ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) <-> ( ph -> ( s e. ( SubGrp ` G ) -> ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) )
39 bi2.04 
 |-  ( ( s C. u -> ( ph -> ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) <-> ( ph -> ( s C. u -> ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) )
40 bi2.04 
 |-  ( ( s e. ( SubGrp ` G ) -> ( ph -> ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) <-> ( ph -> ( s e. ( SubGrp ` G ) -> ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) )
41 38 39 40 3bitr4i 
 |-  ( ( s C. u -> ( ph -> ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) <-> ( s e. ( SubGrp ` G ) -> ( ph -> ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) )
42 41 albii 
 |-  ( A. s ( s C. u -> ( ph -> ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) <-> A. s ( s e. ( SubGrp ` G ) -> ( ph -> ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) )
43 df-ral 
 |-  ( A. s e. ( SubGrp ` G ) ( ph -> ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) <-> A. s ( s e. ( SubGrp ` G ) -> ( ph -> ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) )
44 r19.21v 
 |-  ( A. s e. ( SubGrp ` G ) ( ph -> ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) <-> ( ph -> A. s e. ( SubGrp ` G ) ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) )
45 42 43 44 3bitr2i 
 |-  ( A. s ( s C. u -> ( ph -> ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) <-> ( ph -> A. s e. ( SubGrp ` G ) ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) )
46 psseq1 
 |-  ( x = s -> ( x C. u <-> s C. u ) )
47 eleq2 
 |-  ( x = s -> ( A e. x <-> A e. s ) )
48 46 47 anbi12d 
 |-  ( x = s -> ( ( x C. u /\ A e. x ) <-> ( s C. u /\ A e. s ) ) )
49 ineq2 
 |-  ( y = t -> ( S i^i y ) = ( S i^i t ) )
50 49 eqeq1d 
 |-  ( y = t -> ( ( S i^i y ) = { .0. } <-> ( S i^i t ) = { .0. } ) )
51 oveq2 
 |-  ( y = t -> ( S .(+) y ) = ( S .(+) t ) )
52 51 eqeq1d 
 |-  ( y = t -> ( ( S .(+) y ) = x <-> ( S .(+) t ) = x ) )
53 50 52 anbi12d 
 |-  ( y = t -> ( ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) <-> ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = x ) ) )
54 53 cbvrexvw 
 |-  ( E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) <-> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = x ) )
55 eqeq2 
 |-  ( x = s -> ( ( S .(+) t ) = x <-> ( S .(+) t ) = s ) )
56 55 anbi2d 
 |-  ( x = s -> ( ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = x ) <-> ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) )
57 56 rexbidv 
 |-  ( x = s -> ( E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = x ) <-> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) )
58 54 57 syl5bb 
 |-  ( x = s -> ( E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) <-> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) )
59 48 58 imbi12d 
 |-  ( x = s -> ( ( ( x C. u /\ A e. x ) -> E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) ) <-> ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) )
60 59 cbvralvw 
 |-  ( A. x e. ( SubGrp ` G ) ( ( x C. u /\ A e. x ) -> E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) ) <-> A. s e. ( SubGrp ` G ) ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) )
61 8 adantr 
 |-  ( ( ph /\ ( A. x e. ( SubGrp ` G ) ( ( x C. u /\ A e. x ) -> E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) ) /\ ( u e. ( SubGrp ` G ) /\ A e. u ) ) ) -> P pGrp G )
62 9 adantr 
 |-  ( ( ph /\ ( A. x e. ( SubGrp ` G ) ( ( x C. u /\ A e. x ) -> E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) ) /\ ( u e. ( SubGrp ` G ) /\ A e. u ) ) ) -> G e. Abel )
63 10 adantr 
 |-  ( ( ph /\ ( A. x e. ( SubGrp ` G ) ( ( x C. u /\ A e. x ) -> E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) ) /\ ( u e. ( SubGrp ` G ) /\ A e. u ) ) ) -> B e. Fin )
64 11 adantr 
 |-  ( ( ph /\ ( A. x e. ( SubGrp ` G ) ( ( x C. u /\ A e. x ) -> E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) ) /\ ( u e. ( SubGrp ` G ) /\ A e. u ) ) ) -> ( O ` A ) = E )
65 simprrl 
 |-  ( ( ph /\ ( A. x e. ( SubGrp ` G ) ( ( x C. u /\ A e. x ) -> E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) ) /\ ( u e. ( SubGrp ` G ) /\ A e. u ) ) ) -> u e. ( SubGrp ` G ) )
66 simprrr 
 |-  ( ( ph /\ ( A. x e. ( SubGrp ` G ) ( ( x C. u /\ A e. x ) -> E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) ) /\ ( u e. ( SubGrp ` G ) /\ A e. u ) ) ) -> A e. u )
67 simprl 
 |-  ( ( ph /\ ( A. x e. ( SubGrp ` G ) ( ( x C. u /\ A e. x ) -> E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) ) /\ ( u e. ( SubGrp ` G ) /\ A e. u ) ) ) -> A. x e. ( SubGrp ` G ) ( ( x C. u /\ A e. x ) -> E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) ) )
68 67 60 sylib 
 |-  ( ( ph /\ ( A. x e. ( SubGrp ` G ) ( ( x C. u /\ A e. x ) -> E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) ) /\ ( u e. ( SubGrp ` G ) /\ A e. u ) ) ) -> A. s e. ( SubGrp ` G ) ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) )
69 1 2 3 4 5 6 7 61 62 63 64 65 66 68 pgpfac1lem5 
 |-  ( ( ph /\ ( A. x e. ( SubGrp ` G ) ( ( x C. u /\ A e. x ) -> E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) ) /\ ( u e. ( SubGrp ` G ) /\ A e. u ) ) ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = u ) )
70 69 exp32 
 |-  ( ph -> ( A. x e. ( SubGrp ` G ) ( ( x C. u /\ A e. x ) -> E. y e. ( SubGrp ` G ) ( ( S i^i y ) = { .0. } /\ ( S .(+) y ) = x ) ) -> ( ( u e. ( SubGrp ` G ) /\ A e. u ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = u ) ) ) )
71 60 70 syl5bir 
 |-  ( ph -> ( A. s e. ( SubGrp ` G ) ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) -> ( ( u e. ( SubGrp ` G ) /\ A e. u ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = u ) ) ) )
72 71 a2i 
 |-  ( ( ph -> A. s e. ( SubGrp ` G ) ( ( s C. u /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) -> ( ph -> ( ( u e. ( SubGrp ` G ) /\ A e. u ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = u ) ) ) )
73 45 72 sylbi 
 |-  ( A. s ( s C. u -> ( ph -> ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) -> ( ph -> ( ( u e. ( SubGrp ` G ) /\ A e. u ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = u ) ) ) )
74 73 a1i 
 |-  ( u e. Fin -> ( A. s ( s C. u -> ( ph -> ( ( s e. ( SubGrp ` G ) /\ A e. s ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = s ) ) ) ) -> ( ph -> ( ( u e. ( SubGrp ` G ) /\ A e. u ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = u ) ) ) ) )
75 23 31 74 findcard3 
 |-  ( B e. Fin -> ( ph -> ( ( B e. ( SubGrp ` G ) /\ A e. B ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = B ) ) ) )
76 10 75 mpcom 
 |-  ( ph -> ( ( B e. ( SubGrp ` G ) /\ A e. B ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = B ) ) )
77 15 12 76 mp2and 
 |-  ( ph -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = B ) )