Proof of Theorem pgpfaclem1
Step | Hyp | Ref
| Expression |
1 | | pgpfac.t |
. . 3
++ |
2 | | pgpfac.2 |
. . 3
Word |
3 | | pgpfac.u |
. . . . . . . . 9
SubGrp |
4 | | pgpfac.h |
. . . . . . . . . 10
↾s |
5 | 4 | subggrp 17597 |
. . . . . . . . 9
SubGrp
|
6 | 3, 5 | syl 17 |
. . . . . . . 8
|
7 | | eqid 2622 |
. . . . . . . . 9
|
8 | 7 | subgacs 17629 |
. . . . . . . 8
SubGrp ACS |
9 | | acsmre 16313 |
. . . . . . . 8
SubGrp ACS SubGrp Moore |
10 | 6, 8, 9 | 3syl 18 |
. . . . . . 7
SubGrp Moore |
11 | | pgpfac.x |
. . . . . . . 8
|
12 | 4 | subgbas 17598 |
. . . . . . . . 9
SubGrp
|
13 | 3, 12 | syl 17 |
. . . . . . . 8
|
14 | 11, 13 | eleqtrd 2703 |
. . . . . . 7
|
15 | | pgpfac.k |
. . . . . . . 8
mrClsSubGrp |
16 | 15 | mrcsncl 16272 |
. . . . . . 7
SubGrp Moore
SubGrp |
17 | 10, 14, 16 | syl2anc 693 |
. . . . . 6
SubGrp |
18 | 4 | subsubg 17617 |
. . . . . . 7
SubGrp
SubGrp
SubGrp |
19 | 3, 18 | syl 17 |
. . . . . 6
SubGrp SubGrp |
20 | 17, 19 | mpbid 222 |
. . . . 5
SubGrp |
21 | 20 | simpld 475 |
. . . 4
SubGrp |
22 | 4 | oveq1i 6660 |
. . . . . . 7
↾s ↾s ↾s |
23 | 20 | simprd 479 |
. . . . . . . 8
|
24 | | ressabs 15939 |
. . . . . . . 8
SubGrp
↾s
↾s ↾s |
25 | 3, 23, 24 | syl2anc 693 |
. . . . . . 7
↾s ↾s
↾s |
26 | 22, 25 | syl5eq 2668 |
. . . . . 6
↾s ↾s |
27 | 7, 15 | cycsubgcyg2 18303 |
. . . . . . 7
↾s CycGrp |
28 | 6, 14, 27 | syl2anc 693 |
. . . . . 6
↾s CycGrp |
29 | 26, 28 | eqeltrrd 2702 |
. . . . 5
↾s CycGrp |
30 | | pgpfac.p |
. . . . . . 7
pGrp |
31 | | pgpprm 18008 |
. . . . . . 7
pGrp
|
32 | 30, 31 | syl 17 |
. . . . . 6
|
33 | | subgpgp 18012 |
. . . . . . 7
pGrp SubGrp pGrp
↾s |
34 | 30, 21, 33 | syl2anc 693 |
. . . . . 6
pGrp ↾s |
35 | | brelrng 5355 |
. . . . . 6
↾s CycGrp
pGrp ↾s ↾s pGrp |
36 | 32, 29, 34, 35 | syl3anc 1326 |
. . . . 5
↾s pGrp
|
37 | 29, 36 | elind 3798 |
. . . 4
↾s CycGrp pGrp |
38 | | oveq2 6658 |
. . . . . 6
↾s
↾s |
39 | 38 | eleq1d 2686 |
. . . . 5
↾s CycGrp pGrp
↾s CycGrp pGrp |
40 | | pgpfac.c |
. . . . 5
SubGrp ↾s CycGrp pGrp |
41 | 39, 40 | elrab2 3366 |
. . . 4
SubGrp ↾s CycGrp
pGrp |
42 | 21, 37, 41 | sylanbrc 698 |
. . 3
|
43 | 1, 2, 42 | cats1cld 13600 |
. 2
Word |
44 | | wrdf 13310 |
. . . . 5
Word ..^ |
45 | 43, 44 | syl 17 |
. . . 4
..^ |
46 | | ssrab2 3687 |
. . . . 5
SubGrp ↾s CycGrp pGrp
SubGrp |
47 | 40, 46 | eqsstri 3635 |
. . . 4
SubGrp |
48 | | fss 6056 |
. . . 4
..^ SubGrp ..^SubGrp |
49 | 45, 47, 48 | sylancl 694 |
. . 3
..^SubGrp |
50 | | fzodisj 12502 |
. . . 4
..^ ..^ |
51 | | lencl 13324 |
. . . . . . . 8
Word |
52 | 2, 51 | syl 17 |
. . . . . . 7
|
53 | 52 | nn0zd 11480 |
. . . . . 6
|
54 | | fzosn 12538 |
. . . . . 6
..^ |
55 | 53, 54 | syl 17 |
. . . . 5
..^ |
56 | 55 | ineq2d 3814 |
. . . 4
..^
..^ ..^ |
57 | 50, 56 | syl5reqr 2671 |
. . 3
..^
|
58 | 1 | fveq2i 6194 |
. . . . . . 7
++ |
59 | 42 | s1cld 13383 |
. . . . . . . 8
Word |
60 | | ccatlen 13360 |
. . . . . . . 8
Word Word
++ |
61 | 2, 59, 60 | syl2anc 693 |
. . . . . . 7
++ |
62 | 58, 61 | syl5eq 2668 |
. . . . . 6
|
63 | | s1len 13385 |
. . . . . . 7
|
64 | 63 | oveq2i 6661 |
. . . . . 6
|
65 | 62, 64 | syl6eq 2672 |
. . . . 5
|
66 | 65 | oveq2d 6666 |
. . . 4
..^ ..^ |
67 | | nn0uz 11722 |
. . . . . 6
|
68 | 52, 67 | syl6eleq 2711 |
. . . . 5
|
69 | | fzosplitsn 12576 |
. . . . 5
..^ ..^ |
70 | 68, 69 | syl 17 |
. . . 4
..^ ..^ |
71 | 66, 70 | eqtrd 2656 |
. . 3
..^ ..^ |
72 | | eqid 2622 |
. . 3
Cntz Cntz |
73 | | eqid 2622 |
. . 3
|
74 | | pgpfac.4 |
. . . 4
DProd
|
75 | | cats1un 13475 |
. . . . . . . 8
Word
++ |
76 | 2, 42, 75 | syl2anc 693 |
. . . . . . 7
++
|
77 | 1, 76 | syl5eq 2668 |
. . . . . 6
|
78 | 77 | reseq1d 5395 |
. . . . 5
..^ ..^ |
79 | | wrdf 13310 |
. . . . . . 7
Word ..^ |
80 | | ffn 6045 |
. . . . . . 7
..^ ..^ |
81 | 2, 79, 80 | 3syl 18 |
. . . . . 6
..^ |
82 | | fzonel 12483 |
. . . . . 6
..^ |
83 | | fsnunres 6454 |
. . . . . 6
..^ ..^ ..^ |
84 | 81, 82, 83 | sylancl 694 |
. . . . 5
..^ |
85 | 78, 84 | eqtrd 2656 |
. . . 4
..^ |
86 | 74, 85 | breqtrrd 4681 |
. . 3
DProd
..^ |
87 | | fvex 6201 |
. . . . . 6
|
88 | | dprdsn 18435 |
. . . . . 6
SubGrp DProd DProd |
89 | 87, 21, 88 | sylancr 695 |
. . . . 5
DProd DProd |
90 | 89 | simpld 475 |
. . . 4
DProd
|
91 | | ffn 6045 |
. . . . . . 7
..^ ..^ |
92 | 43, 44, 91 | 3syl 18 |
. . . . . 6
..^ |
93 | | ssun2 3777 |
. . . . . . . 8
..^ |
94 | 87 | snss 4316 |
. . . . . . . 8
..^
..^ |
95 | 93, 94 | mpbir 221 |
. . . . . . 7
..^ |
96 | 95, 71 | syl5eleqr 2708 |
. . . . . 6
..^ |
97 | | fnressn 6425 |
. . . . . 6
..^ ..^ |
98 | 92, 96, 97 | syl2anc 693 |
. . . . 5
|
99 | 1 | fveq1i 6192 |
. . . . . . . . 9
++ |
100 | 52 | nn0cnd 11353 |
. . . . . . . . . . . 12
|
101 | 100 | addid2d 10237 |
. . . . . . . . . . 11
|
102 | 101 | eqcomd 2628 |
. . . . . . . . . 10
|
103 | 102 | fveq2d 6195 |
. . . . . . . . 9
++ ++ |
104 | 99, 103 | syl5eq 2668 |
. . . . . . . 8
++ |
105 | | 1nn 11031 |
. . . . . . . . . . . 12
|
106 | 105 | a1i 11 |
. . . . . . . . . . 11
|
107 | 63, 106 | syl5eqel 2705 |
. . . . . . . . . 10
|
108 | | lbfzo0 12507 |
. . . . . . . . . 10
..^
|
109 | 107, 108 | sylibr 224 |
. . . . . . . . 9
..^ |
110 | | ccatval3 13363 |
. . . . . . . . 9
Word Word
..^ ++ |
111 | 2, 59, 109, 110 | syl3anc 1326 |
. . . . . . . 8
++ |
112 | | fvex 6201 |
. . . . . . . . 9
|
113 | | s1fv 13390 |
. . . . . . . . 9
|
114 | 112, 113 | mp1i 13 |
. . . . . . . 8
|
115 | 104, 111,
114 | 3eqtrd 2660 |
. . . . . . 7
|
116 | 115 | opeq2d 4409 |
. . . . . 6
|
117 | 116 | sneqd 4189 |
. . . . 5
|
118 | 98, 117 | eqtrd 2656 |
. . . 4
|
119 | 90, 118 | breqtrrd 4681 |
. . 3
DProd
|
120 | | pgpfac.g |
. . . 4
|
121 | | dprdsubg 18423 |
. . . . 5
DProd ..^ DProd
..^ SubGrp |
122 | 86, 121 | syl 17 |
. . . 4
DProd ..^ SubGrp |
123 | | dprdsubg 18423 |
. . . . 5
DProd DProd
SubGrp |
124 | 119, 123 | syl 17 |
. . . 4
DProd SubGrp |
125 | 72, 120, 122, 124 | ablcntzd 18260 |
. . 3
DProd ..^
Cntz DProd |
126 | | pgpfac.i |
. . . 4
|
127 | 85 | oveq2d 6666 |
. . . . . . 7
DProd ..^ DProd |
128 | | pgpfac.5 |
. . . . . . 7
DProd |
129 | 127, 128 | eqtrd 2656 |
. . . . . 6
DProd ..^ |
130 | 118 | oveq2d 6666 |
. . . . . . 7
DProd DProd |
131 | 89 | simprd 479 |
. . . . . . 7
DProd |
132 | 130, 131 | eqtrd 2656 |
. . . . . 6
DProd |
133 | 129, 132 | ineq12d 3815 |
. . . . 5
DProd ..^ DProd |
134 | | incom 3805 |
. . . . 5
|
135 | 133, 134 | syl6eq 2672 |
. . . 4
DProd ..^ DProd |
136 | 4, 73 | subg0 17600 |
. . . . . . 7
SubGrp
|
137 | 3, 136 | syl 17 |
. . . . . 6
|
138 | | pgpfac.0 |
. . . . . 6
|
139 | 137, 138 | syl6eqr 2674 |
. . . . 5
|
140 | 139 | sneqd 4189 |
. . . 4
|
141 | 126, 135,
140 | 3eqtr4d 2666 |
. . 3
DProd ..^ DProd |
142 | 49, 57, 71, 72, 73, 86, 119, 125, 141 | dmdprdsplit2 18445 |
. 2
DProd
|
143 | | eqid 2622 |
. . . . 5
|
144 | 49, 57, 71, 143, 142 | dprdsplit 18447 |
. . . 4
DProd DProd ..^ DProd
|
145 | 129, 132 | oveq12d 6668 |
. . . 4
DProd ..^ DProd |
146 | 129, 122 | eqeltrrd 2702 |
. . . . 5
SubGrp |
147 | 143 | lsmcom 18261 |
. . . . 5
SubGrp SubGrp |
148 | 120, 146,
21, 147 | syl3anc 1326 |
. . . 4
|
149 | 144, 145,
148 | 3eqtrd 2660 |
. . 3
DProd |
150 | | pgpfac.w |
. . . . . 6
SubGrp |
151 | 7 | subgss 17595 |
. . . . . 6
SubGrp
|
152 | 150, 151 | syl 17 |
. . . . 5
|
153 | 152, 13 | sseqtr4d 3642 |
. . . 4
|
154 | | pgpfac.l |
. . . . 5
|
155 | 4, 143, 154 | subglsm 18086 |
. . . 4
SubGrp
|
156 | 3, 23, 153, 155 | syl3anc 1326 |
. . 3
|
157 | | pgpfac.s |
. . 3
|
158 | 149, 156,
157 | 3eqtrd 2660 |
. 2
DProd |
159 | | breq2 4657 |
. . . 4
DProd
DProd |
160 | | oveq2 6658 |
. . . . 5
DProd DProd |
161 | 160 | eqeq1d 2624 |
. . . 4
DProd
DProd |
162 | 159, 161 | anbi12d 747 |
. . 3
DProd
DProd
DProd DProd |
163 | 162 | rspcev 3309 |
. 2
Word DProd
DProd
Word DProd
DProd |
164 | 43, 142, 158, 163 | syl12anc 1324 |
1
Word DProd
DProd |