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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablfac1.o ⊢ 𝑂 = ( od ‘ 𝐺 )
ablfac1.s ⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
ablfac1.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
ablfac1.f ⊢ ( 𝜑 → 𝐵 ∈ Fin )
ablfac1.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℙ )
ablfac1c.d ⊢ 𝐷 = { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) }
ablfac1.2 ⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 )
Assertion ablfac1c ( 𝜑 → ( 𝐺 DProd 𝑆 ) = 𝐵 )

Proof

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