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 ˙ = 0 G
pgpfac1.l ⊢ ⊕ ˙ = LSSum ⁡ G
pgpfac1.p ⊢ φ → P pGrp G
pgpfac1.g ⊢ φ → G ∈ Abel
pgpfac1.n ⊢ φ → B ∈ Fin
pgpfac1.oe ⊢ φ → O ⁡ A = E
pgpfac1.ab ⊢ φ → A ∈ B
Assertion pgpfac1 ⊢ φ → ∃ t ∈ SubGrp ⁡ G S ∩ 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 ˙ = 0 G
7 pgpfac1.l ⊢ ⊕ ˙ = LSSum ⁡ G
8 pgpfac1.p ⊢ φ → P pGrp G
9 pgpfac1.g ⊢ φ → G ∈ Abel
10 pgpfac1.n ⊢ φ → B ∈ Fin
11 pgpfac1.oe ⊢ φ → O ⁡ A = E
12 pgpfac1.ab ⊢ φ → A ∈ B
13 ablgrp ⊢ G ∈ Abel → G ∈ Grp
14 3 subgid ⊢ G ∈ Grp → B ∈ SubGrp ⁡ G
15 9 13 14 3syl ⊢ φ → B ∈ SubGrp ⁡ G
16 eleq1 ⊢ s = u → s ∈ SubGrp ⁡ G ↔ u ∈ SubGrp ⁡ G
17 eleq2 ⊢ s = u → A ∈ s ↔ A ∈ u
18 16 17 anbi12d ⊢ s = u → s ∈ SubGrp ⁡ G ∧ A ∈ s ↔ u ∈ SubGrp ⁡ G ∧ A ∈ u
19 eqeq2 ⊢ s = u → S ⊕ ˙ t = s ↔ S ⊕ ˙ t = u
20 19 anbi2d ⊢ s = u → S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = u
21 20 rexbidv ⊢ s = u → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = u
22 18 21 imbi12d ⊢ s = u → s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ u ∈ SubGrp ⁡ G ∧ A ∈ u → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = u
23 22 imbi2d ⊢ s = u → φ → s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ φ → u ∈ SubGrp ⁡ G ∧ A ∈ u → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = u
24 eleq1 ⊢ s = B → s ∈ SubGrp ⁡ G ↔ B ∈ SubGrp ⁡ G
25 eleq2 ⊢ s = B → A ∈ s ↔ A ∈ B
26 24 25 anbi12d ⊢ s = B → s ∈ SubGrp ⁡ G ∧ A ∈ s ↔ B ∈ SubGrp ⁡ G ∧ A ∈ B
27 eqeq2 ⊢ s = B → S ⊕ ˙ t = s ↔ S ⊕ ˙ t = B
28 27 anbi2d ⊢ s = B → S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = B
29 28 rexbidv ⊢ s = B → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = B
30 26 29 imbi12d ⊢ s = B → s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ B ∈ SubGrp ⁡ G ∧ A ∈ B → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = B
31 30 imbi2d ⊢ s = B → φ → s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ φ → B ∈ SubGrp ⁡ G ∧ A ∈ B → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = B
32 bi2.04 ⊢ s ⊂ u → s ∈ SubGrp ⁡ G → A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ s ∈ SubGrp ⁡ G → s ⊂ u → A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
33 impexp ⊢ s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ s ∈ SubGrp ⁡ G → A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
34 33 imbi2i ⊢ s ⊂ u → s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ s ⊂ u → s ∈ SubGrp ⁡ G → A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
35 impexp ⊢ s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ s ⊂ u → A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
36 35 imbi2i ⊢ s ∈ SubGrp ⁡ G → s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ s ∈ SubGrp ⁡ G → s ⊂ u → A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
37 32 34 36 3bitr4i ⊢ s ⊂ u → s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ s ∈ SubGrp ⁡ G → s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
38 37 imbi2i ⊢ φ → s ⊂ u → s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ φ → s ∈ SubGrp ⁡ G → s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
39 bi2.04 ⊢ s ⊂ u → φ → s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ φ → s ⊂ u → s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
40 bi2.04 ⊢ s ∈ SubGrp ⁡ G → φ → s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ φ → s ∈ SubGrp ⁡ G → s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
41 38 39 40 3bitr4i ⊢ s ⊂ u → φ → s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ s ∈ SubGrp ⁡ G → φ → s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
42 41 albii ⊢ ∀ s s ⊂ u → φ → s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ ∀ s s ∈ SubGrp ⁡ G → φ → s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
43 df-ral ⊢ ∀ s ∈ SubGrp ⁡ G φ → s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ ∀ s s ∈ SubGrp ⁡ G → φ → s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
44 r19.21v ⊢ ∀ s ∈ SubGrp ⁡ G φ → s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ φ → ∀ s ∈ SubGrp ⁡ G s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
45 42 43 44 3bitr2i ⊢ ∀ s s ⊂ u → φ → s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s ↔ φ → ∀ s ∈ SubGrp ⁡ G s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
46 psseq1 ⊢ x = s → x ⊂ u ↔ s ⊂ u
47 eleq2 ⊢ x = s → A ∈ x ↔ A ∈ s
48 46 47 anbi12d ⊢ x = s → x ⊂ u ∧ A ∈ x ↔ s ⊂ u ∧ A ∈ s
49 ineq2 ⊢ y = t → S ∩ y = S ∩ t
50 49 eqeq1d ⊢ y = t → S ∩ y = 0 ˙ ↔ S ∩ 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 ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x ↔ S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = x
54 53 cbvrexvw ⊢ ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x ↔ ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = x
55 eqeq2 ⊢ x = s → S ⊕ ˙ t = x ↔ S ⊕ ˙ t = s
56 55 anbi2d ⊢ x = s → S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = x ↔ S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
57 56 rexbidv ⊢ x = s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = x ↔ ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
58 54 57 syl5bb ⊢ x = s → ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x ↔ ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
59 48 58 imbi12d ⊢ x = s → x ⊂ u ∧ A ∈ x → ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x ↔ s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
60 59 cbvralvw ⊢ ∀ x ∈ SubGrp ⁡ G x ⊂ u ∧ A ∈ x → ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x ↔ ∀ s ∈ SubGrp ⁡ G s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
61 8 adantr ⊢ φ ∧ ∀ x ∈ SubGrp ⁡ G x ⊂ u ∧ A ∈ x → ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x ∧ u ∈ SubGrp ⁡ G ∧ A ∈ u → P pGrp G
62 9 adantr ⊢ φ ∧ ∀ x ∈ SubGrp ⁡ G x ⊂ u ∧ A ∈ x → ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x ∧ u ∈ SubGrp ⁡ G ∧ A ∈ u → G ∈ Abel
63 10 adantr ⊢ φ ∧ ∀ x ∈ SubGrp ⁡ G x ⊂ u ∧ A ∈ x → ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x ∧ u ∈ SubGrp ⁡ G ∧ A ∈ u → B ∈ Fin
64 11 adantr ⊢ φ ∧ ∀ x ∈ SubGrp ⁡ G x ⊂ u ∧ A ∈ x → ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x ∧ u ∈ SubGrp ⁡ G ∧ A ∈ u → O ⁡ A = E
65 simprrl ⊢ φ ∧ ∀ x ∈ SubGrp ⁡ G x ⊂ u ∧ A ∈ x → ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x ∧ u ∈ SubGrp ⁡ G ∧ A ∈ u → u ∈ SubGrp ⁡ G
66 simprrr ⊢ φ ∧ ∀ x ∈ SubGrp ⁡ G x ⊂ u ∧ A ∈ x → ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x ∧ u ∈ SubGrp ⁡ G ∧ A ∈ u → A ∈ u
67 simprl ⊢ φ ∧ ∀ x ∈ SubGrp ⁡ G x ⊂ u ∧ A ∈ x → ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x ∧ u ∈ SubGrp ⁡ G ∧ A ∈ u → ∀ x ∈ SubGrp ⁡ G x ⊂ u ∧ A ∈ x → ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x
68 67 60 sylib ⊢ φ ∧ ∀ x ∈ SubGrp ⁡ G x ⊂ u ∧ A ∈ x → ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x ∧ u ∈ SubGrp ⁡ G ∧ A ∈ u → ∀ s ∈ SubGrp ⁡ G s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s
69 1 2 3 4 5 6 7 61 62 63 64 65 66 68 pgpfac1lem5 ⊢ φ ∧ ∀ x ∈ SubGrp ⁡ G x ⊂ u ∧ A ∈ x → ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x ∧ u ∈ SubGrp ⁡ G ∧ A ∈ u → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = u
70 69 exp32 ⊢ φ → ∀ x ∈ SubGrp ⁡ G x ⊂ u ∧ A ∈ x → ∃ y ∈ SubGrp ⁡ G S ∩ y = 0 ˙ ∧ S ⊕ ˙ y = x → u ∈ SubGrp ⁡ G ∧ A ∈ u → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = u
71 60 70 syl5bir ⊢ φ → ∀ s ∈ SubGrp ⁡ G s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s → u ∈ SubGrp ⁡ G ∧ A ∈ u → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = u
72 71 a2i ⊢ φ → ∀ s ∈ SubGrp ⁡ G s ⊂ u ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s → φ → u ∈ SubGrp ⁡ G ∧ A ∈ u → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = u
73 45 72 sylbi ⊢ ∀ s s ⊂ u → φ → s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s → φ → u ∈ SubGrp ⁡ G ∧ A ∈ u → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = u
74 73 a1i ⊢ u ∈ Fin → ∀ s s ⊂ u → φ → s ∈ SubGrp ⁡ G ∧ A ∈ s → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = s → φ → u ∈ SubGrp ⁡ G ∧ A ∈ u → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = u
75 23 31 74 findcard3 ⊢ B ∈ Fin → φ → B ∈ SubGrp ⁡ G ∧ A ∈ B → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = B
76 10 75 mpcom ⊢ φ → B ∈ SubGrp ⁡ G ∧ A ∈ B → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = B
77 15 12 76 mp2and ⊢ φ → ∃ t ∈ SubGrp ⁡ G S ∩ t = 0 ˙ ∧ S ⊕ ˙ t = B