Step | Hyp | Ref
| Expression |
1 | | pgpfac.w |
. . . . . 6
SubGrp |
2 | | pgpfac.u |
. . . . . . 7
SubGrp |
3 | | pgpfac.h |
. . . . . . . 8
↾s |
4 | 3 | subsubg 17617 |
. . . . . . 7
SubGrp
SubGrp SubGrp |
5 | 2, 4 | syl 17 |
. . . . . 6
SubGrp
SubGrp
|
6 | 1, 5 | mpbid 222 |
. . . . 5
SubGrp |
7 | 6 | simpld 475 |
. . . 4
SubGrp |
8 | | pgpfac.a |
. . . 4
SubGrp Word DProd DProd |
9 | 6 | simprd 479 |
. . . . 5
|
10 | | pgpfac.f |
. . . . . . . . . . 11
|
11 | | pgpfac.b |
. . . . . . . . . . . . 13
|
12 | 11 | subgss 17595 |
. . . . . . . . . . . 12
SubGrp
|
13 | 2, 12 | syl 17 |
. . . . . . . . . . 11
|
14 | | ssfi 8180 |
. . . . . . . . . . 11
|
15 | 10, 13, 14 | syl2anc 693 |
. . . . . . . . . 10
|
16 | | ssfi 8180 |
. . . . . . . . . 10
|
17 | 15, 9, 16 | syl2anc 693 |
. . . . . . . . 9
|
18 | | hashcl 13147 |
. . . . . . . . 9
|
19 | 17, 18 | syl 17 |
. . . . . . . 8
|
20 | 19 | nn0red 11352 |
. . . . . . 7
|
21 | | pgpfac.0 |
. . . . . . . . . . . 12
|
22 | | fvex 6201 |
. . . . . . . . . . . 12
|
23 | 21, 22 | eqeltri 2697 |
. . . . . . . . . . 11
|
24 | | hashsng 13159 |
. . . . . . . . . . 11
|
25 | 23, 24 | ax-mp 5 |
. . . . . . . . . 10
|
26 | | subgrcl 17599 |
. . . . . . . . . . . . . . . 16
SubGrp
|
27 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
28 | 27 | subgacs 17629 |
. . . . . . . . . . . . . . . 16
SubGrp ACS |
29 | | acsmre 16313 |
. . . . . . . . . . . . . . . 16
SubGrp ACS SubGrp Moore |
30 | 1, 26, 28, 29 | 4syl 19 |
. . . . . . . . . . . . . . 15
SubGrp Moore |
31 | | pgpfac.k |
. . . . . . . . . . . . . . 15
mrClsSubGrp |
32 | 30, 31 | mrcssvd 16283 |
. . . . . . . . . . . . . 14
|
33 | 3 | subgbas 17598 |
. . . . . . . . . . . . . . 15
SubGrp
|
34 | 2, 33 | syl 17 |
. . . . . . . . . . . . . 14
|
35 | 32, 34 | sseqtr4d 3642 |
. . . . . . . . . . . . 13
|
36 | | ssfi 8180 |
. . . . . . . . . . . . 13
|
37 | 15, 35, 36 | syl2anc 693 |
. . . . . . . . . . . 12
|
38 | | pgpfac.x |
. . . . . . . . . . . . . . . . 17
|
39 | 38, 34 | eleqtrd 2703 |
. . . . . . . . . . . . . . . 16
|
40 | 31 | mrcsncl 16272 |
. . . . . . . . . . . . . . . 16
SubGrp Moore
SubGrp |
41 | 30, 39, 40 | syl2anc 693 |
. . . . . . . . . . . . . . 15
SubGrp |
42 | 21 | subg0cl 17602 |
. . . . . . . . . . . . . . 15
SubGrp |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . 14
|
44 | 43 | snssd 4340 |
. . . . . . . . . . . . 13
|
45 | 39 | snssd 4340 |
. . . . . . . . . . . . . . 15
|
46 | 30, 31, 45 | mrcssidd 16285 |
. . . . . . . . . . . . . 14
|
47 | | snssg 4327 |
. . . . . . . . . . . . . . 15
|
48 | 38, 47 | syl 17 |
. . . . . . . . . . . . . 14
|
49 | 46, 48 | mpbird 247 |
. . . . . . . . . . . . 13
|
50 | | pgpfac.oe |
. . . . . . . . . . . . . . 15
|
51 | | pgpfac.1 |
. . . . . . . . . . . . . . 15
|
52 | 50, 51 | eqnetrd 2861 |
. . . . . . . . . . . . . 14
|
53 | | pgpfac.o |
. . . . . . . . . . . . . . . . . 18
|
54 | 53, 21 | od1 17976 |
. . . . . . . . . . . . . . . . 17
|
55 | 1, 26, 54 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
56 | | elsni 4194 |
. . . . . . . . . . . . . . . . . 18
|
57 | 56 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
58 | 57 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
|
59 | 55, 58 | syl5ibrcom 237 |
. . . . . . . . . . . . . . 15
|
60 | 59 | necon3ad 2807 |
. . . . . . . . . . . . . 14
|
61 | 52, 60 | mpd 15 |
. . . . . . . . . . . . 13
|
62 | 44, 49, 61 | ssnelpssd 3719 |
. . . . . . . . . . . 12
|
63 | | php3 8146 |
. . . . . . . . . . . 12
|
64 | 37, 62, 63 | syl2anc 693 |
. . . . . . . . . . 11
|
65 | | snfi 8038 |
. . . . . . . . . . . 12
|
66 | | hashsdom 13170 |
. . . . . . . . . . . 12
|
67 | 65, 37, 66 | sylancr 695 |
. . . . . . . . . . 11
|
68 | 64, 67 | mpbird 247 |
. . . . . . . . . 10
|
69 | 25, 68 | syl5eqbrr 4689 |
. . . . . . . . 9
|
70 | | 1red 10055 |
. . . . . . . . . 10
|
71 | | hashcl 13147 |
. . . . . . . . . . . 12
|
72 | 37, 71 | syl 17 |
. . . . . . . . . . 11
|
73 | 72 | nn0red 11352 |
. . . . . . . . . 10
|
74 | 21 | subg0cl 17602 |
. . . . . . . . . . . . 13
SubGrp
|
75 | | ne0i 3921 |
. . . . . . . . . . . . 13
|
76 | 1, 74, 75 | 3syl 18 |
. . . . . . . . . . . 12
|
77 | | hashnncl 13157 |
. . . . . . . . . . . . 13
|
78 | 17, 77 | syl 17 |
. . . . . . . . . . . 12
|
79 | 76, 78 | mpbird 247 |
. . . . . . . . . . 11
|
80 | 79 | nngt0d 11064 |
. . . . . . . . . 10
|
81 | | ltmul1 10873 |
. . . . . . . . . 10
|
82 | 70, 73, 20, 80, 81 | syl112anc 1330 |
. . . . . . . . 9
|
83 | 69, 82 | mpbid 222 |
. . . . . . . 8
|
84 | 20 | recnd 10068 |
. . . . . . . . 9
|
85 | 84 | mulid2d 10058 |
. . . . . . . 8
|
86 | | pgpfac.l |
. . . . . . . . . 10
|
87 | | eqid 2622 |
. . . . . . . . . 10
Cntz Cntz |
88 | | pgpfac.i |
. . . . . . . . . 10
|
89 | | pgpfac.g |
. . . . . . . . . . . 12
|
90 | 3 | subgabl 18241 |
. . . . . . . . . . . 12
SubGrp
|
91 | 89, 2, 90 | syl2anc 693 |
. . . . . . . . . . 11
|
92 | 87, 91, 41, 1 | ablcntzd 18260 |
. . . . . . . . . 10
Cntz |
93 | 86, 21, 87, 41, 1, 88, 92, 37, 17 | lsmhash 18118 |
. . . . . . . . 9
|
94 | | pgpfac.s |
. . . . . . . . . 10
|
95 | 94 | fveq2d 6195 |
. . . . . . . . 9
|
96 | 93, 95 | eqtr3d 2658 |
. . . . . . . 8
|
97 | 83, 85, 96 | 3brtr3d 4684 |
. . . . . . 7
|
98 | 20, 97 | ltned 10173 |
. . . . . 6
|
99 | | fveq2 6191 |
. . . . . . 7
|
100 | 99 | necon3i 2826 |
. . . . . 6
|
101 | 98, 100 | syl 17 |
. . . . 5
|
102 | | df-pss 3590 |
. . . . 5
|
103 | 9, 101, 102 | sylanbrc 698 |
. . . 4
|
104 | | psseq1 3694 |
. . . . . 6
|
105 | | eqeq2 2633 |
. . . . . . . 8
DProd
DProd |
106 | 105 | anbi2d 740 |
. . . . . . 7
DProd
DProd
DProd DProd |
107 | 106 | rexbidv 3052 |
. . . . . 6
Word DProd
DProd
Word DProd DProd |
108 | 104, 107 | imbi12d 334 |
. . . . 5
Word DProd
DProd Word DProd
DProd |
109 | 108 | rspcv 3305 |
. . . 4
SubGrp
SubGrp Word DProd
DProd Word DProd
DProd |
110 | 7, 8, 103, 109 | syl3c 66 |
. . 3
Word DProd
DProd |
111 | | breq2 4657 |
. . . . 5
DProd
DProd |
112 | | oveq2 6658 |
. . . . . 6
DProd DProd |
113 | 112 | eqeq1d 2624 |
. . . . 5
DProd
DProd |
114 | 111, 113 | anbi12d 747 |
. . . 4
DProd
DProd
DProd DProd |
115 | 114 | cbvrexv 3172 |
. . 3
Word DProd
DProd
Word DProd DProd |
116 | 110, 115 | sylib 208 |
. 2
Word DProd
DProd |
117 | | pgpfac.c |
. . 3
SubGrp ↾s CycGrp pGrp |
118 | 89 | adantr 481 |
. . 3
Word DProd DProd
|
119 | | pgpfac.p |
. . . 4
pGrp |
120 | 119 | adantr 481 |
. . 3
Word DProd DProd pGrp |
121 | 10 | adantr 481 |
. . 3
Word DProd DProd
|
122 | 2 | adantr 481 |
. . 3
Word DProd DProd
SubGrp |
123 | 8 | adantr 481 |
. . 3
Word DProd DProd
SubGrp Word DProd DProd |
124 | | pgpfac.e |
. . 3
gEx |
125 | 51 | adantr 481 |
. . 3
Word DProd DProd |
126 | 38 | adantr 481 |
. . 3
Word DProd DProd
|
127 | 50 | adantr 481 |
. . 3
Word DProd DProd |
128 | 1 | adantr 481 |
. . 3
Word DProd DProd
SubGrp |
129 | 88 | adantr 481 |
. . 3
Word DProd DProd |
130 | 94 | adantr 481 |
. . 3
Word DProd DProd |
131 | | simprl 794 |
. . 3
Word DProd DProd Word
|
132 | | simprrl 804 |
. . 3
Word DProd DProd DProd |
133 | | simprrr 805 |
. . 3
Word DProd DProd DProd
|
134 | | eqid 2622 |
. . 3
++ ++ |
135 | 11, 117, 118, 120, 121, 122, 123, 3, 31, 53, 124, 21, 86, 125, 126, 127, 128, 129, 130, 131, 132, 133, 134 | pgpfaclem1 18480 |
. 2
Word DProd DProd
Word DProd
DProd |
136 | 116, 135 | rexlimddv 3035 |
1
Word DProd
DProd |