Metamath Proof Explorer

Theorem ablfac1c

Description: The factors of ablfac1b cover the entire group. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses ablfac1.b ⊢B=BaseG
ablfac1.o ⊢O=od⁡G
ablfac1.s ⊢S=p∈A⟼x∈B|O⁡x∥pppCntB
ablfac1.g ⊢φ→G∈Abel
ablfac1.f ⊢φ→B∈Fin
ablfac1.1 ⊢φ→A⊆ℙ
ablfac1c.d ⊢D=w∈ℙ|w∥B
ablfac1.2 ⊢φ→D⊆A
Assertion ablfac1c ⊢φ→GDProdS=B

Proof

Step Hyp Ref Expression
1 ablfac1.b ⊢B=BaseG
2 ablfac1.o ⊢O=od⁡G
3 ablfac1.s ⊢S=p∈A⟼x∈B|O⁡x∥pppCntB
4 ablfac1.g ⊢φ→G∈Abel
5 ablfac1.f ⊢φ→B∈Fin
6 ablfac1.1 ⊢φ→A⊆ℙ
7 ablfac1c.d ⊢D=w∈ℙ|w∥B
8 ablfac1.2 ⊢φ→D⊆A
9 1 dprdssv ⊢GDProdS⊆B
10 9 a1i ⊢φ→GDProdS⊆B
11 ssfi ⊢B∈Fin∧GDProdS⊆B→GDProdS∈Fin
12 5 9 11 sylancl ⊢φ→GDProdS∈Fin
13 hashcl ⊢GDProdS∈Fin→GDProdS∈ℕ0
14 12 13 syl ⊢φ→GDProdS∈ℕ0
15 hashcl ⊢B∈Fin→B∈ℕ0
16 5 15 syl ⊢φ→B∈ℕ0
17 1 2 3 4 5 6 ablfac1b ⊢φ→Gdom⁡DProdS
18 dprdsubg ⊢Gdom⁡DProdS→GDProdS∈SubGrp⁡G
19 17 18 syl ⊢φ→GDProdS∈SubGrp⁡G
20 1 lagsubg ⊢GDProdS∈SubGrp⁡G∧B∈Fin→GDProdS∥B
21 19 5 20 syl2anc ⊢φ→GDProdS∥B
22 breq1 ⊢w=q→w∥B↔q∥B
23 22 7 elrab2 ⊢q∈D↔q∈ℙ∧q∥B
24 8 sseld ⊢φ→q∈D→q∈A
25 23 24 biimtrrid ⊢φ→q∈ℙ∧q∥B→q∈A
26 25 impl ⊢φ∧q∈ℙ∧q∥B→q∈A
27 1 2 3 4 5 6 ablfac1a ⊢φ∧q∈A→S⁡q=qqpCntB
28 1 fvexi ⊢B∈V
29 28 rabex ⊢x∈B|O⁡x∥pppCntB∈V
30 29 3 dmmpti ⊢dom⁡S=A
31 30 a1i ⊢φ→dom⁡S=A
32 17 31 dprdf2 ⊢φ→S:A⟶SubGrp⁡G
33 32 ffvelcdmda ⊢φ∧q∈A→S⁡q∈SubGrp⁡G
34 17 adantr ⊢φ∧q∈A→Gdom⁡DProdS
35 30 a1i ⊢φ∧q∈A→dom⁡S=A
36 simpr ⊢φ∧q∈A→q∈A
37 34 35 36 dprdub ⊢φ∧q∈A→S⁡q⊆GDProdS
38 19 adantr ⊢φ∧q∈A→GDProdS∈SubGrp⁡G
39 eqid ⊢G↾𝑠GDProdS=G↾𝑠GDProdS
40 39 subsubg ⊢GDProdS∈SubGrp⁡G→S⁡q∈SubGrp⁡G↾𝑠GDProdS↔S⁡q∈SubGrp⁡G∧S⁡q⊆GDProdS
41 38 40 syl ⊢φ∧q∈A→S⁡q∈SubGrp⁡G↾𝑠GDProdS↔S⁡q∈SubGrp⁡G∧S⁡q⊆GDProdS
42 33 37 41 mpbir2and ⊢φ∧q∈A→S⁡q∈SubGrp⁡G↾𝑠GDProdS
43 39 subgbas ⊢GDProdS∈SubGrp⁡G→GDProdS=BaseG↾𝑠GDProdS
44 38 43 syl ⊢φ∧q∈A→GDProdS=BaseG↾𝑠GDProdS
45 12 adantr ⊢φ∧q∈A→GDProdS∈Fin
46 44 45 eqeltrrd ⊢φ∧q∈A→BaseG↾𝑠GDProdS∈Fin
47 eqid ⊢BaseG↾𝑠GDProdS=BaseG↾𝑠GDProdS
48 47 lagsubg ⊢S⁡q∈SubGrp⁡G↾𝑠GDProdS∧BaseG↾𝑠GDProdS∈Fin→S⁡q∥BaseG↾𝑠GDProdS
49 42 46 48 syl2anc ⊢φ∧q∈A→S⁡q∥BaseG↾𝑠GDProdS
50 44 fveq2d ⊢φ∧q∈A→GDProdS=BaseG↾𝑠GDProdS
51 49 50 breqtrrd ⊢φ∧q∈A→S⁡q∥GDProdS
52 27 51 eqbrtrrd ⊢φ∧q∈A→qqpCntB∥GDProdS
53 6 sselda ⊢φ∧q∈A→q∈ℙ
54 14 nn0zd ⊢φ→GDProdS∈ℤ
55 54 adantr ⊢φ∧q∈A→GDProdS∈ℤ
56 simpr ⊢φ∧q∈ℙ→q∈ℙ
57 ablgrp ⊢G∈Abel→G∈Grp
58 1 grpbn0 ⊢G∈Grp→B≠∅
59 4 57 58 3syl ⊢φ→B≠∅
60 hashnncl ⊢B∈Fin→B∈ℕ↔B≠∅
61 5 60 syl ⊢φ→B∈ℕ↔B≠∅
62 59 61 mpbird ⊢φ→B∈ℕ
63 62 adantr ⊢φ∧q∈ℙ→B∈ℕ
64 56 63 pccld ⊢φ∧q∈ℙ→qpCntB∈ℕ0
65 53 64 syldan ⊢φ∧q∈A→qpCntB∈ℕ0
66 pcdvdsb ⊢q∈ℙ∧GDProdS∈ℤ∧qpCntB∈ℕ0→qpCntB≤qpCntGDProdS↔qqpCntB∥GDProdS
67 53 55 65 66 syl3anc ⊢φ∧q∈A→qpCntB≤qpCntGDProdS↔qqpCntB∥GDProdS
68 52 67 mpbird ⊢φ∧q∈A→qpCntB≤qpCntGDProdS
69 68 adantlr ⊢φ∧q∈ℙ∧q∈A→qpCntB≤qpCntGDProdS
70 26 69 syldan ⊢φ∧q∈ℙ∧q∥B→qpCntB≤qpCntGDProdS
71 pceq0 ⊢q∈ℙ∧B∈ℕ→qpCntB=0↔¬q∥B
72 56 63 71 syl2anc ⊢φ∧q∈ℙ→qpCntB=0↔¬q∥B
73 72 biimpar ⊢φ∧q∈ℙ∧¬q∥B→qpCntB=0
74 eqid ⊢0G=0G
75 74 subg0cl ⊢GDProdS∈SubGrp⁡G→0G∈GDProdS
76 ne0i ⊢0G∈GDProdS→GDProdS≠∅
77 19 75 76 3syl ⊢φ→GDProdS≠∅
78 hashnncl ⊢GDProdS∈Fin→GDProdS∈ℕ↔GDProdS≠∅
79 12 78 syl ⊢φ→GDProdS∈ℕ↔GDProdS≠∅
80 77 79 mpbird ⊢φ→GDProdS∈ℕ
81 80 adantr ⊢φ∧q∈ℙ→GDProdS∈ℕ
82 56 81 pccld ⊢φ∧q∈ℙ→qpCntGDProdS∈ℕ0
83 82 nn0ge0d ⊢φ∧q∈ℙ→0≤qpCntGDProdS
84 83 adantr ⊢φ∧q∈ℙ∧¬q∥B→0≤qpCntGDProdS
85 73 84 eqbrtrd ⊢φ∧q∈ℙ∧¬q∥B→qpCntB≤qpCntGDProdS
86 70 85 pm2.61dan ⊢φ∧q∈ℙ→qpCntB≤qpCntGDProdS
87 86 ralrimiva ⊢φ→∀q∈ℙqpCntB≤qpCntGDProdS
88 16 nn0zd ⊢φ→B∈ℤ
89 pc2dvds ⊢B∈ℤ∧GDProdS∈ℤ→B∥GDProdS↔∀q∈ℙqpCntB≤qpCntGDProdS
90 88 54 89 syl2anc ⊢φ→B∥GDProdS↔∀q∈ℙqpCntB≤qpCntGDProdS
91 87 90 mpbird ⊢φ→B∥GDProdS
92 dvdseq ⊢GDProdS∈ℕ0∧B∈ℕ0∧GDProdS∥B∧B∥GDProdS→GDProdS=B
93 14 16 21 91 92 syl22anc ⊢φ→GDProdS=B
94 hashen ⊢GDProdS∈Fin∧B∈Fin→GDProdS=B↔GDProdS≈B
95 12 5 94 syl2anc ⊢φ→GDProdS=B↔GDProdS≈B
96 93 95 mpbid ⊢φ→GDProdS≈B
97 fisseneq ⊢B∈Fin∧GDProdS⊆B∧GDProdS≈B→GDProdS=B
98 5 10 96 97 syl3anc ⊢φ→GDProdS=B