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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
pgpfac.c ⊢ 𝐶 = { 𝑟 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝐺 ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) }
pgpfac.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
pgpfac.p ⊢ ( 𝜑 → 𝑃 pGrp 𝐺 )
pgpfac.f ⊢ ( 𝜑 → 𝐵 ∈ Fin )
Assertion pgpfac ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 pgpfac.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 pgpfac.c ⊢ 𝐶 = { 𝑟 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝐺 ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) }
3 pgpfac.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
4 pgpfac.p ⊢ ( 𝜑 → 𝑃 pGrp 𝐺 )
5 pgpfac.f ⊢ ( 𝜑 → 𝐵 ∈ Fin )
6 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
7 1 subgid ⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) )
8 3 6 7 3syl ⊢ ( 𝜑 → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) )
9 eleq1 ⊢ ( 𝑡 = 𝑢 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ↔ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) )
10 eqeq2 ⊢ ( 𝑡 = 𝑢 → ( ( 𝐺 DProd 𝑠 ) = 𝑡 ↔ ( 𝐺 DProd 𝑠 ) = 𝑢 ) )
11 10 anbi2d ⊢ ( 𝑡 = 𝑢 → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) )
12 11 rexbidv ⊢ ( 𝑡 = 𝑢 → ( ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) )
13 9 12 imbi12d ⊢ ( 𝑡 = 𝑢 → ( ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ↔ ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) ) )
14 13 imbi2d ⊢ ( 𝑡 = 𝑢 → ( ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ↔ ( 𝜑 → ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) ) ) )
15 eleq1 ⊢ ( 𝑡 = 𝐵 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ↔ 𝐵 ∈ ( SubGrp ‘ 𝐺 ) ) )
16 eqeq2 ⊢ ( 𝑡 = 𝐵 → ( ( 𝐺 DProd 𝑠 ) = 𝑡 ↔ ( 𝐺 DProd 𝑠 ) = 𝐵 ) )
17 16 anbi2d ⊢ ( 𝑡 = 𝐵 → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) )
18 17 rexbidv ⊢ ( 𝑡 = 𝐵 → ( ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) )
19 15 18 imbi12d ⊢ ( 𝑡 = 𝐵 → ( ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ↔ ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ) )
20 19 imbi2d ⊢ ( 𝑡 = 𝐵 → ( ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ↔ ( 𝜑 → ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ) ) )
21 bi2.04 ⊢ ( ( 𝑡 ⊊ 𝑢 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ↔ ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) )
22 21 imbi2i ⊢ ( ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ↔ ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) )
23 bi2.04 ⊢ ( ( 𝑡 ⊊ 𝑢 → ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ↔ ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) )
24 bi2.04 ⊢ ( ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ↔ ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) )
25 22 23 24 3bitr4i ⊢ ( ( 𝑡 ⊊ 𝑢 → ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ↔ ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) )
26 25 albii ⊢ ( ∀ 𝑡 ( 𝑡 ⊊ 𝑢 → ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ↔ ∀ 𝑡 ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) )
27 df-ral ⊢ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ↔ ∀ 𝑡 ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) )
28 r19.21v ⊢ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝜑 → ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ↔ ( 𝜑 → ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) )
29 26 27 28 3bitr2i ⊢ ( ∀ 𝑡 ( 𝑡 ⊊ 𝑢 → ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) ↔ ( 𝜑 → ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) )
30 3 adantr ⊢ ( ( 𝜑 ∧ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ∧ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) → 𝐺 ∈ Abel )
31 4 adantr ⊢ ( ( 𝜑 ∧ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ∧ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) → 𝑃 pGrp 𝐺 )
32 5 adantr ⊢ ( ( 𝜑 ∧ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ∧ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) → 𝐵 ∈ Fin )
33 simprr ⊢ ( ( 𝜑 ∧ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ∧ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) → 𝑢 ∈ ( SubGrp ‘ 𝐺 ) )
34 simprl ⊢ ( ( 𝜑 ∧ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ∧ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) )
35 psseq1 ⊢ ( 𝑡 = 𝑥 → ( 𝑡 ⊊ 𝑢 ↔ 𝑥 ⊊ 𝑢 ) )
36 eqeq2 ⊢ ( 𝑡 = 𝑥 → ( ( 𝐺 DProd 𝑠 ) = 𝑡 ↔ ( 𝐺 DProd 𝑠 ) = 𝑥 ) )
37 36 anbi2d ⊢ ( 𝑡 = 𝑥 → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑥 ) ) )
38 37 rexbidv ⊢ ( 𝑡 = 𝑥 → ( ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑥 ) ) )
39 35 38 imbi12d ⊢ ( 𝑡 = 𝑥 → ( ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ↔ ( 𝑥 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑥 ) ) ) )
40 39 cbvralvw ⊢ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ↔ ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑥 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑥 ) ) )
41 34 40 sylib ⊢ ( ( 𝜑 ∧ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ∧ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ∀ 𝑥 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑥 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑥 ) ) )
42 1 2 30 31 32 33 41 pgpfaclem3 ⊢ ( ( 𝜑 ∧ ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ∧ 𝑢 ∈ ( SubGrp ‘ 𝐺 ) ) ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) )
43 42 exp32 ⊢ ( 𝜑 → ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) → ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) ) )
44 43 a1i ⊢ ( 𝑢 ∈ Fin → ( 𝜑 → ( ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) → ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) ) ) )
45 44 a2d ⊢ ( 𝑢 ∈ Fin → ( ( 𝜑 → ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑢 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) → ( 𝜑 → ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) ) ) )
46 29 45 biimtrid ⊢ ( 𝑢 ∈ Fin → ( ∀ 𝑡 ( 𝑡 ⊊ 𝑢 → ( 𝜑 → ( 𝑡 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ) ) → ( 𝜑 → ( 𝑢 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑢 ) ) ) ) )
47 14 20 46 findcard3 ⊢ ( 𝐵 ∈ Fin → ( 𝜑 → ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ) )
48 5 47 mpcom ⊢ ( 𝜑 → ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) )
49 8 48 mpd ⊢ ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) )