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=mrClsSubGrpG
pgpfac1.s S=KA
pgpfac1.b B=BaseG
pgpfac1.o O=odG
pgpfac1.e E=gExG
pgpfac1.z 0˙=0G
pgpfac1.l ˙=LSSumG
pgpfac1.p φPpGrpG
pgpfac1.g φGAbel
pgpfac1.n φBFin
pgpfac1.oe φOA=E
pgpfac1.ab φAB
Assertion pgpfac1 φtSubGrpGSt=0˙S˙t=B

Proof

Step Hyp Ref Expression
1 pgpfac1.k K=mrClsSubGrpG
2 pgpfac1.s S=KA
3 pgpfac1.b B=BaseG
4 pgpfac1.o O=odG
5 pgpfac1.e E=gExG
6 pgpfac1.z 0˙=0G
7 pgpfac1.l ˙=LSSumG
8 pgpfac1.p φPpGrpG
9 pgpfac1.g φGAbel
10 pgpfac1.n φBFin
11 pgpfac1.oe φOA=E
12 pgpfac1.ab φAB
13 ablgrp GAbelGGrp
14 3 subgid GGrpBSubGrpG
15 9 13 14 3syl φBSubGrpG
16 eleq1 s=usSubGrpGuSubGrpG
17 eleq2 s=uAsAu
18 16 17 anbi12d s=usSubGrpGAsuSubGrpGAu
19 eqeq2 s=uS˙t=sS˙t=u
20 19 anbi2d s=uSt=0˙S˙t=sSt=0˙S˙t=u
21 20 rexbidv s=utSubGrpGSt=0˙S˙t=stSubGrpGSt=0˙S˙t=u
22 18 21 imbi12d s=usSubGrpGAstSubGrpGSt=0˙S˙t=suSubGrpGAutSubGrpGSt=0˙S˙t=u
23 22 imbi2d s=uφsSubGrpGAstSubGrpGSt=0˙S˙t=sφuSubGrpGAutSubGrpGSt=0˙S˙t=u
24 eleq1 s=BsSubGrpGBSubGrpG
25 eleq2 s=BAsAB
26 24 25 anbi12d s=BsSubGrpGAsBSubGrpGAB
27 eqeq2 s=BS˙t=sS˙t=B
28 27 anbi2d s=BSt=0˙S˙t=sSt=0˙S˙t=B
29 28 rexbidv s=BtSubGrpGSt=0˙S˙t=stSubGrpGSt=0˙S˙t=B
30 26 29 imbi12d s=BsSubGrpGAstSubGrpGSt=0˙S˙t=sBSubGrpGABtSubGrpGSt=0˙S˙t=B
31 30 imbi2d s=BφsSubGrpGAstSubGrpGSt=0˙S˙t=sφBSubGrpGABtSubGrpGSt=0˙S˙t=B
32 bi2.04 susSubGrpGAstSubGrpGSt=0˙S˙t=ssSubGrpGsuAstSubGrpGSt=0˙S˙t=s
33 impexp sSubGrpGAstSubGrpGSt=0˙S˙t=ssSubGrpGAstSubGrpGSt=0˙S˙t=s
34 33 imbi2i susSubGrpGAstSubGrpGSt=0˙S˙t=ssusSubGrpGAstSubGrpGSt=0˙S˙t=s
35 impexp suAstSubGrpGSt=0˙S˙t=ssuAstSubGrpGSt=0˙S˙t=s
36 35 imbi2i sSubGrpGsuAstSubGrpGSt=0˙S˙t=ssSubGrpGsuAstSubGrpGSt=0˙S˙t=s
37 32 34 36 3bitr4i susSubGrpGAstSubGrpGSt=0˙S˙t=ssSubGrpGsuAstSubGrpGSt=0˙S˙t=s
38 37 imbi2i φsusSubGrpGAstSubGrpGSt=0˙S˙t=sφsSubGrpGsuAstSubGrpGSt=0˙S˙t=s
39 bi2.04 suφsSubGrpGAstSubGrpGSt=0˙S˙t=sφsusSubGrpGAstSubGrpGSt=0˙S˙t=s
40 bi2.04 sSubGrpGφsuAstSubGrpGSt=0˙S˙t=sφsSubGrpGsuAstSubGrpGSt=0˙S˙t=s
41 38 39 40 3bitr4i suφsSubGrpGAstSubGrpGSt=0˙S˙t=ssSubGrpGφsuAstSubGrpGSt=0˙S˙t=s
42 41 albii ssuφsSubGrpGAstSubGrpGSt=0˙S˙t=sssSubGrpGφsuAstSubGrpGSt=0˙S˙t=s
43 df-ral sSubGrpGφsuAstSubGrpGSt=0˙S˙t=sssSubGrpGφsuAstSubGrpGSt=0˙S˙t=s
44 r19.21v sSubGrpGφsuAstSubGrpGSt=0˙S˙t=sφsSubGrpGsuAstSubGrpGSt=0˙S˙t=s
45 42 43 44 3bitr2i ssuφsSubGrpGAstSubGrpGSt=0˙S˙t=sφsSubGrpGsuAstSubGrpGSt=0˙S˙t=s
46 psseq1 x=sxusu
47 eleq2 x=sAxAs
48 46 47 anbi12d x=sxuAxsuAs
49 ineq2 y=tSy=St
50 49 eqeq1d y=tSy=0˙St=0˙
51 oveq2 y=tS˙y=S˙t
52 51 eqeq1d y=tS˙y=xS˙t=x
53 50 52 anbi12d y=tSy=0˙S˙y=xSt=0˙S˙t=x
54 53 cbvrexvw ySubGrpGSy=0˙S˙y=xtSubGrpGSt=0˙S˙t=x
55 eqeq2 x=sS˙t=xS˙t=s
56 55 anbi2d x=sSt=0˙S˙t=xSt=0˙S˙t=s
57 56 rexbidv x=stSubGrpGSt=0˙S˙t=xtSubGrpGSt=0˙S˙t=s
58 54 57 syl5bb x=sySubGrpGSy=0˙S˙y=xtSubGrpGSt=0˙S˙t=s
59 48 58 imbi12d x=sxuAxySubGrpGSy=0˙S˙y=xsuAstSubGrpGSt=0˙S˙t=s
60 59 cbvralvw xSubGrpGxuAxySubGrpGSy=0˙S˙y=xsSubGrpGsuAstSubGrpGSt=0˙S˙t=s
61 8 adantr φxSubGrpGxuAxySubGrpGSy=0˙S˙y=xuSubGrpGAuPpGrpG
62 9 adantr φxSubGrpGxuAxySubGrpGSy=0˙S˙y=xuSubGrpGAuGAbel
63 10 adantr φxSubGrpGxuAxySubGrpGSy=0˙S˙y=xuSubGrpGAuBFin
64 11 adantr φxSubGrpGxuAxySubGrpGSy=0˙S˙y=xuSubGrpGAuOA=E
65 simprrl φxSubGrpGxuAxySubGrpGSy=0˙S˙y=xuSubGrpGAuuSubGrpG
66 simprrr φxSubGrpGxuAxySubGrpGSy=0˙S˙y=xuSubGrpGAuAu
67 simprl φxSubGrpGxuAxySubGrpGSy=0˙S˙y=xuSubGrpGAuxSubGrpGxuAxySubGrpGSy=0˙S˙y=x
68 67 60 sylib φxSubGrpGxuAxySubGrpGSy=0˙S˙y=xuSubGrpGAusSubGrpGsuAstSubGrpGSt=0˙S˙t=s
69 1 2 3 4 5 6 7 61 62 63 64 65 66 68 pgpfac1lem5 φxSubGrpGxuAxySubGrpGSy=0˙S˙y=xuSubGrpGAutSubGrpGSt=0˙S˙t=u
70 69 exp32 φxSubGrpGxuAxySubGrpGSy=0˙S˙y=xuSubGrpGAutSubGrpGSt=0˙S˙t=u
71 60 70 syl5bir φsSubGrpGsuAstSubGrpGSt=0˙S˙t=suSubGrpGAutSubGrpGSt=0˙S˙t=u
72 71 a2i φsSubGrpGsuAstSubGrpGSt=0˙S˙t=sφuSubGrpGAutSubGrpGSt=0˙S˙t=u
73 45 72 sylbi ssuφsSubGrpGAstSubGrpGSt=0˙S˙t=sφuSubGrpGAutSubGrpGSt=0˙S˙t=u
74 73 a1i uFinssuφsSubGrpGAstSubGrpGSt=0˙S˙t=sφuSubGrpGAutSubGrpGSt=0˙S˙t=u
75 23 31 74 findcard3 BFinφBSubGrpGABtSubGrpGSt=0˙S˙t=B
76 10 75 mpcom φBSubGrpGABtSubGrpGSt=0˙S˙t=B
77 15 12 76 mp2and φtSubGrpGSt=0˙S˙t=B