Step | Hyp | Ref
| Expression |
1 | | pgpfac.w |
. . . . . . 7
β’ (π β π β (SubGrpβπ»)) |
2 | | pgpfac.u |
. . . . . . . 8
β’ (π β π β (SubGrpβπΊ)) |
3 | | pgpfac.h |
. . . . . . . . 9
β’ π» = (πΊ βΎs π) |
4 | 3 | subsubg 18951 |
. . . . . . . 8
β’ (π β (SubGrpβπΊ) β (π β (SubGrpβπ») β (π β (SubGrpβπΊ) β§ π β π))) |
5 | 2, 4 | syl 17 |
. . . . . . 7
β’ (π β (π β (SubGrpβπ») β (π β (SubGrpβπΊ) β§ π β π))) |
6 | 1, 5 | mpbid 231 |
. . . . . 6
β’ (π β (π β (SubGrpβπΊ) β§ π β π)) |
7 | 6 | simprd 496 |
. . . . 5
β’ (π β π β π) |
8 | | pgpfac.f |
. . . . . . . . . . 11
β’ (π β π΅ β Fin) |
9 | | pgpfac.b |
. . . . . . . . . . . . 13
β’ π΅ = (BaseβπΊ) |
10 | 9 | subgss 18929 |
. . . . . . . . . . . 12
β’ (π β (SubGrpβπΊ) β π β π΅) |
11 | 2, 10 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β π΅) |
12 | 8, 11 | ssfid 9211 |
. . . . . . . . . 10
β’ (π β π β Fin) |
13 | 12, 7 | ssfid 9211 |
. . . . . . . . 9
β’ (π β π β Fin) |
14 | | hashcl 14256 |
. . . . . . . . 9
β’ (π β Fin β
(β―βπ) β
β0) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
β’ (π β (β―βπ) β
β0) |
16 | 15 | nn0red 12474 |
. . . . . . 7
β’ (π β (β―βπ) β
β) |
17 | | pgpfac.0 |
. . . . . . . . . . . 12
β’ 0 =
(0gβπ») |
18 | 17 | fvexi 6856 |
. . . . . . . . . . 11
β’ 0 β
V |
19 | | hashsng 14269 |
. . . . . . . . . . 11
β’ ( 0 β V
β (β―β{ 0 }) = 1) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . 10
β’
(β―β{ 0 }) = 1 |
21 | | subgrcl 18933 |
. . . . . . . . . . . . . . . 16
β’ (π β (SubGrpβπ») β π» β Grp) |
22 | | eqid 2736 |
. . . . . . . . . . . . . . . . 17
β’
(Baseβπ») =
(Baseβπ») |
23 | 22 | subgacs 18963 |
. . . . . . . . . . . . . . . 16
β’ (π» β Grp β
(SubGrpβπ») β
(ACSβ(Baseβπ»))) |
24 | | acsmre 17532 |
. . . . . . . . . . . . . . . 16
β’
((SubGrpβπ»)
β (ACSβ(Baseβπ»)) β (SubGrpβπ») β (Mooreβ(Baseβπ»))) |
25 | 1, 21, 23, 24 | 4syl 19 |
. . . . . . . . . . . . . . 15
β’ (π β (SubGrpβπ») β
(Mooreβ(Baseβπ»))) |
26 | | pgpfac.k |
. . . . . . . . . . . . . . 15
β’ πΎ =
(mrClsβ(SubGrpβπ»)) |
27 | 25, 26 | mrcssvd 17503 |
. . . . . . . . . . . . . 14
β’ (π β (πΎβ{π}) β (Baseβπ»)) |
28 | 3 | subgbas 18932 |
. . . . . . . . . . . . . . 15
β’ (π β (SubGrpβπΊ) β π = (Baseβπ»)) |
29 | 2, 28 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π = (Baseβπ»)) |
30 | 27, 29 | sseqtrrd 3985 |
. . . . . . . . . . . . 13
β’ (π β (πΎβ{π}) β π) |
31 | 12, 30 | ssfid 9211 |
. . . . . . . . . . . 12
β’ (π β (πΎβ{π}) β Fin) |
32 | | pgpfac.x |
. . . . . . . . . . . . . . . . 17
β’ (π β π β π) |
33 | 32, 29 | eleqtrd 2839 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (Baseβπ»)) |
34 | 26 | mrcsncl 17492 |
. . . . . . . . . . . . . . . 16
β’
(((SubGrpβπ»)
β (Mooreβ(Baseβπ»)) β§ π β (Baseβπ»)) β (πΎβ{π}) β (SubGrpβπ»)) |
35 | 25, 33, 34 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’ (π β (πΎβ{π}) β (SubGrpβπ»)) |
36 | 17 | subg0cl 18936 |
. . . . . . . . . . . . . . 15
β’ ((πΎβ{π}) β (SubGrpβπ») β 0 β (πΎβ{π})) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β 0 β (πΎβ{π})) |
38 | 37 | snssd 4769 |
. . . . . . . . . . . . 13
β’ (π β { 0 } β (πΎβ{π})) |
39 | 33 | snssd 4769 |
. . . . . . . . . . . . . . 15
β’ (π β {π} β (Baseβπ»)) |
40 | 25, 26, 39 | mrcssidd 17505 |
. . . . . . . . . . . . . 14
β’ (π β {π} β (πΎβ{π})) |
41 | | snssg 4744 |
. . . . . . . . . . . . . . 15
β’ (π β π β (π β (πΎβ{π}) β {π} β (πΎβ{π}))) |
42 | 32, 41 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (π β (πΎβ{π}) β {π} β (πΎβ{π}))) |
43 | 40, 42 | mpbird 256 |
. . . . . . . . . . . . 13
β’ (π β π β (πΎβ{π})) |
44 | | pgpfac.oe |
. . . . . . . . . . . . . . 15
β’ (π β (πβπ) = πΈ) |
45 | | pgpfac.1 |
. . . . . . . . . . . . . . 15
β’ (π β πΈ β 1) |
46 | 44, 45 | eqnetrd 3011 |
. . . . . . . . . . . . . 14
β’ (π β (πβπ) β 1) |
47 | | pgpfac.o |
. . . . . . . . . . . . . . . . . 18
β’ π = (odβπ») |
48 | 47, 17 | od1 19341 |
. . . . . . . . . . . . . . . . 17
β’ (π» β Grp β (πβ 0 ) = 1) |
49 | 1, 21, 48 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ (π β (πβ 0 ) = 1) |
50 | | elsni 4603 |
. . . . . . . . . . . . . . . . 17
β’ (π β { 0 } β π = 0 ) |
51 | 50 | fveqeq2d 6850 |
. . . . . . . . . . . . . . . 16
β’ (π β { 0 } β ((πβπ) = 1 β (πβ 0 ) = 1)) |
52 | 49, 51 | syl5ibrcom 246 |
. . . . . . . . . . . . . . 15
β’ (π β (π β { 0 } β (πβπ) = 1)) |
53 | 52 | necon3ad 2956 |
. . . . . . . . . . . . . 14
β’ (π β ((πβπ) β 1 β Β¬ π β { 0 })) |
54 | 46, 53 | mpd 15 |
. . . . . . . . . . . . 13
β’ (π β Β¬ π β { 0 }) |
55 | 38, 43, 54 | ssnelpssd 4072 |
. . . . . . . . . . . 12
β’ (π β { 0 } β (πΎβ{π})) |
56 | | php3 9156 |
. . . . . . . . . . . 12
β’ (((πΎβ{π}) β Fin β§ { 0 } β (πΎβ{π})) β { 0 } βΊ (πΎβ{π})) |
57 | 31, 55, 56 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β { 0 } βΊ (πΎβ{π})) |
58 | | snfi 8988 |
. . . . . . . . . . . 12
β’ { 0 } β
Fin |
59 | | hashsdom 14281 |
. . . . . . . . . . . 12
β’ (({ 0 } β Fin
β§ (πΎβ{π}) β Fin) β
((β―β{ 0 }) <
(β―β(πΎβ{π})) β { 0 } βΊ (πΎβ{π}))) |
60 | 58, 31, 59 | sylancr 587 |
. . . . . . . . . . 11
β’ (π β ((β―β{ 0 }) <
(β―β(πΎβ{π})) β { 0 } βΊ (πΎβ{π}))) |
61 | 57, 60 | mpbird 256 |
. . . . . . . . . 10
β’ (π β (β―β{ 0 }) <
(β―β(πΎβ{π}))) |
62 | 20, 61 | eqbrtrrid 5141 |
. . . . . . . . 9
β’ (π β 1 <
(β―β(πΎβ{π}))) |
63 | | 1red 11156 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
64 | | hashcl 14256 |
. . . . . . . . . . . 12
β’ ((πΎβ{π}) β Fin β (β―β(πΎβ{π})) β
β0) |
65 | 31, 64 | syl 17 |
. . . . . . . . . . 11
β’ (π β (β―β(πΎβ{π})) β
β0) |
66 | 65 | nn0red 12474 |
. . . . . . . . . 10
β’ (π β (β―β(πΎβ{π})) β β) |
67 | 17 | subg0cl 18936 |
. . . . . . . . . . . . 13
β’ (π β (SubGrpβπ») β 0 β π) |
68 | | ne0i 4294 |
. . . . . . . . . . . . 13
β’ ( 0 β π β π β β
) |
69 | 1, 67, 68 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π β π β β
) |
70 | | hashnncl 14266 |
. . . . . . . . . . . . 13
β’ (π β Fin β
((β―βπ) β
β β π β
β
)) |
71 | 13, 70 | syl 17 |
. . . . . . . . . . . 12
β’ (π β ((β―βπ) β β β π β β
)) |
72 | 69, 71 | mpbird 256 |
. . . . . . . . . . 11
β’ (π β (β―βπ) β
β) |
73 | 72 | nngt0d 12202 |
. . . . . . . . . 10
β’ (π β 0 <
(β―βπ)) |
74 | | ltmul1 12005 |
. . . . . . . . . 10
β’ ((1
β β β§ (β―β(πΎβ{π})) β β β§
((β―βπ) β
β β§ 0 < (β―βπ))) β (1 < (β―β(πΎβ{π})) β (1 Β· (β―βπ)) < ((β―β(πΎβ{π})) Β· (β―βπ)))) |
75 | 63, 66, 16, 73, 74 | syl112anc 1374 |
. . . . . . . . 9
β’ (π β (1 <
(β―β(πΎβ{π})) β (1 Β· (β―βπ)) < ((β―β(πΎβ{π})) Β· (β―βπ)))) |
76 | 62, 75 | mpbid 231 |
. . . . . . . 8
β’ (π β (1 Β·
(β―βπ)) <
((β―β(πΎβ{π})) Β· (β―βπ))) |
77 | 16 | recnd 11183 |
. . . . . . . . 9
β’ (π β (β―βπ) β
β) |
78 | 77 | mulid2d 11173 |
. . . . . . . 8
β’ (π β (1 Β·
(β―βπ)) =
(β―βπ)) |
79 | | pgpfac.l |
. . . . . . . . . 10
β’ β =
(LSSumβπ») |
80 | | eqid 2736 |
. . . . . . . . . 10
β’
(Cntzβπ») =
(Cntzβπ») |
81 | | pgpfac.i |
. . . . . . . . . 10
β’ (π β ((πΎβ{π}) β© π) = { 0 }) |
82 | | pgpfac.g |
. . . . . . . . . . . 12
β’ (π β πΊ β Abel) |
83 | 3 | subgabl 19614 |
. . . . . . . . . . . 12
β’ ((πΊ β Abel β§ π β (SubGrpβπΊ)) β π» β Abel) |
84 | 82, 2, 83 | syl2anc 584 |
. . . . . . . . . . 11
β’ (π β π» β Abel) |
85 | 80, 84, 35, 1 | ablcntzd 19635 |
. . . . . . . . . 10
β’ (π β (πΎβ{π}) β ((Cntzβπ»)βπ)) |
86 | 79, 17, 80, 35, 1, 81, 85, 31, 13 | lsmhash 19487 |
. . . . . . . . 9
β’ (π β (β―β((πΎβ{π}) β π)) = ((β―β(πΎβ{π})) Β· (β―βπ))) |
87 | | pgpfac.s |
. . . . . . . . . 10
β’ (π β ((πΎβ{π}) β π) = π) |
88 | 87 | fveq2d 6846 |
. . . . . . . . 9
β’ (π β (β―β((πΎβ{π}) β π)) = (β―βπ)) |
89 | 86, 88 | eqtr3d 2778 |
. . . . . . . 8
β’ (π β ((β―β(πΎβ{π})) Β· (β―βπ)) = (β―βπ)) |
90 | 76, 78, 89 | 3brtr3d 5136 |
. . . . . . 7
β’ (π β (β―βπ) < (β―βπ)) |
91 | 16, 90 | ltned 11291 |
. . . . . 6
β’ (π β (β―βπ) β (β―βπ)) |
92 | | fveq2 6842 |
. . . . . . 7
β’ (π = π β (β―βπ) = (β―βπ)) |
93 | 92 | necon3i 2976 |
. . . . . 6
β’
((β―βπ)
β (β―βπ)
β π β π) |
94 | 91, 93 | syl 17 |
. . . . 5
β’ (π β π β π) |
95 | | df-pss 3929 |
. . . . 5
β’ (π β π β (π β π β§ π β π)) |
96 | 7, 94, 95 | sylanbrc 583 |
. . . 4
β’ (π β π β π) |
97 | | psseq1 4047 |
. . . . . 6
β’ (π‘ = π β (π‘ β π β π β π)) |
98 | | eqeq2 2748 |
. . . . . . . 8
β’ (π‘ = π β ((πΊ DProd π ) = π‘ β (πΊ DProd π ) = π)) |
99 | 98 | anbi2d 629 |
. . . . . . 7
β’ (π‘ = π β ((πΊdom DProd π β§ (πΊ DProd π ) = π‘) β (πΊdom DProd π β§ (πΊ DProd π ) = π))) |
100 | 99 | rexbidv 3175 |
. . . . . 6
β’ (π‘ = π β (βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π‘) β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π))) |
101 | 97, 100 | imbi12d 344 |
. . . . 5
β’ (π‘ = π β ((π‘ β π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π‘)) β (π β π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π)))) |
102 | | pgpfac.a |
. . . . 5
β’ (π β βπ‘ β (SubGrpβπΊ)(π‘ β π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π‘))) |
103 | 6 | simpld 495 |
. . . . 5
β’ (π β π β (SubGrpβπΊ)) |
104 | 101, 102,
103 | rspcdva 3582 |
. . . 4
β’ (π β (π β π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π))) |
105 | 96, 104 | mpd 15 |
. . 3
β’ (π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π)) |
106 | | breq2 5109 |
. . . . 5
β’ (π = π β (πΊdom DProd π β πΊdom DProd π)) |
107 | | oveq2 7365 |
. . . . . 6
β’ (π = π β (πΊ DProd π ) = (πΊ DProd π)) |
108 | 107 | eqeq1d 2738 |
. . . . 5
β’ (π = π β ((πΊ DProd π ) = π β (πΊ DProd π) = π)) |
109 | 106, 108 | anbi12d 631 |
. . . 4
β’ (π = π β ((πΊdom DProd π β§ (πΊ DProd π ) = π) β (πΊdom DProd π β§ (πΊ DProd π) = π))) |
110 | 109 | cbvrexvw 3226 |
. . 3
β’
(βπ β
Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π) β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π) = π)) |
111 | 105, 110 | sylib 217 |
. 2
β’ (π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π) = π)) |
112 | | pgpfac.c |
. . 3
β’ πΆ = {π β (SubGrpβπΊ) β£ (πΊ βΎs π) β (CycGrp β© ran pGrp
)} |
113 | 82 | adantr 481 |
. . 3
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β πΊ β Abel) |
114 | | pgpfac.p |
. . . 4
β’ (π β π pGrp πΊ) |
115 | 114 | adantr 481 |
. . 3
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β π pGrp πΊ) |
116 | 8 | adantr 481 |
. . 3
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β π΅ β Fin) |
117 | 2 | adantr 481 |
. . 3
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β π β (SubGrpβπΊ)) |
118 | 102 | adantr 481 |
. . 3
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β βπ‘ β (SubGrpβπΊ)(π‘ β π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π‘))) |
119 | | pgpfac.e |
. . 3
β’ πΈ = (gExβπ») |
120 | 45 | adantr 481 |
. . 3
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β πΈ β 1) |
121 | 32 | adantr 481 |
. . 3
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β π β π) |
122 | 44 | adantr 481 |
. . 3
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β (πβπ) = πΈ) |
123 | 1 | adantr 481 |
. . 3
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β π β (SubGrpβπ»)) |
124 | 81 | adantr 481 |
. . 3
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β ((πΎβ{π}) β© π) = { 0 }) |
125 | 87 | adantr 481 |
. . 3
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β ((πΎβ{π}) β π) = π) |
126 | | simprl 769 |
. . 3
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β π β Word πΆ) |
127 | | simprrl 779 |
. . 3
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β πΊdom DProd π) |
128 | | simprrr 780 |
. . 3
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β (πΊ DProd π) = π) |
129 | | eqid 2736 |
. . 3
β’ (π ++ β¨β(πΎβ{π})ββ©) = (π ++ β¨β(πΎβ{π})ββ©) |
130 | 9, 112, 113, 115, 116, 117, 118, 3, 26, 47, 119, 17, 79, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129 | pgpfaclem1 19860 |
. 2
β’ ((π β§ (π β Word πΆ β§ (πΊdom DProd π β§ (πΊ DProd π) = π))) β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π)) |
131 | 111, 130 | rexlimddv 3158 |
1
β’ (π β βπ β Word πΆ(πΊdom DProd π β§ (πΊ DProd π ) = π)) |