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 syl5bi ( 𝑢 ∈ 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 𝑠 ) = 𝐵 ) )