Step | Hyp | Ref
| Expression |
1 | | ablfac1.f |
. 2
|
2 | | ablfac1.b |
. . . 4
|
3 | 2 | dprdssv 18415 |
. . 3
DProd |
4 | 3 | a1i 11 |
. 2
DProd |
5 | | ssfi 8180 |
. . . . . 6
DProd DProd |
6 | 1, 3, 5 | sylancl 694 |
. . . . 5
DProd |
7 | | hashcl 13147 |
. . . . 5
DProd DProd |
8 | 6, 7 | syl 17 |
. . . 4
DProd |
9 | | hashcl 13147 |
. . . . 5
|
10 | 1, 9 | syl 17 |
. . . 4
|
11 | | ablfac1.o |
. . . . . . 7
|
12 | | ablfac1.s |
. . . . . . 7
|
13 | | ablfac1.g |
. . . . . . 7
|
14 | | ablfac1.1 |
. . . . . . 7
|
15 | 2, 11, 12, 13, 1, 14 | ablfac1b 18469 |
. . . . . 6
DProd
|
16 | | dprdsubg 18423 |
. . . . . 6
DProd
DProd SubGrp |
17 | 15, 16 | syl 17 |
. . . . 5
DProd SubGrp |
18 | 2 | lagsubg 17656 |
. . . . 5
DProd SubGrp
DProd |
19 | 17, 1, 18 | syl2anc 693 |
. . . 4
DProd |
20 | | breq1 4656 |
. . . . . . . . . . 11
|
21 | | ablfac1c.d |
. . . . . . . . . . 11
|
22 | 20, 21 | elrab2 3366 |
. . . . . . . . . 10
|
23 | | ablfac1.2 |
. . . . . . . . . . 11
|
24 | 23 | sseld 3602 |
. . . . . . . . . 10
|
25 | 22, 24 | syl5bir 233 |
. . . . . . . . 9
|
26 | 25 | impl 650 |
. . . . . . . 8
|
27 | 2, 11, 12, 13, 1, 14 | ablfac1a 18468 |
. . . . . . . . . . 11
|
28 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
|
29 | 2, 28 | eqeltri 2697 |
. . . . . . . . . . . . . . . . . . 19
|
30 | 29 | rabex 4813 |
. . . . . . . . . . . . . . . . . 18
|
31 | 30, 12 | dmmpti 6023 |
. . . . . . . . . . . . . . . . 17
|
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
33 | 15, 32 | dprdf2 18406 |
. . . . . . . . . . . . . . 15
SubGrp |
34 | 33 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
SubGrp |
35 | 15 | adantr 481 |
. . . . . . . . . . . . . . 15
DProd |
36 | 31 | a1i 11 |
. . . . . . . . . . . . . . 15
|
37 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
38 | 35, 36, 37 | dprdub 18424 |
. . . . . . . . . . . . . 14
DProd |
39 | 17 | adantr 481 |
. . . . . . . . . . . . . . 15
DProd SubGrp |
40 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
↾s DProd ↾s DProd |
41 | 40 | subsubg 17617 |
. . . . . . . . . . . . . . 15
DProd SubGrp SubGrp
↾s DProd
SubGrp
DProd |
42 | 39, 41 | syl 17 |
. . . . . . . . . . . . . 14
SubGrp
↾s DProd
SubGrp
DProd |
43 | 34, 38, 42 | mpbir2and 957 |
. . . . . . . . . . . . 13
SubGrp ↾s DProd |
44 | 40 | subgbas 17598 |
. . . . . . . . . . . . . . 15
DProd SubGrp DProd ↾s
DProd |
45 | 39, 44 | syl 17 |
. . . . . . . . . . . . . 14
DProd ↾s DProd |
46 | 6 | adantr 481 |
. . . . . . . . . . . . . 14
DProd |
47 | 45, 46 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
↾s DProd |
48 | | eqid 2622 |
. . . . . . . . . . . . . 14
↾s DProd ↾s
DProd |
49 | 48 | lagsubg 17656 |
. . . . . . . . . . . . 13
SubGrp
↾s DProd ↾s DProd ↾s DProd |
50 | 43, 47, 49 | syl2anc 693 |
. . . . . . . . . . . 12
↾s DProd |
51 | 45 | fveq2d 6195 |
. . . . . . . . . . . 12
DProd
↾s DProd |
52 | 50, 51 | breqtrrd 4681 |
. . . . . . . . . . 11
DProd |
53 | 27, 52 | eqbrtrrd 4677 |
. . . . . . . . . 10
DProd |
54 | 14 | sselda 3603 |
. . . . . . . . . . 11
|
55 | 8 | nn0zd 11480 |
. . . . . . . . . . . 12
DProd |
56 | 55 | adantr 481 |
. . . . . . . . . . 11
DProd |
57 | | simpr 477 |
. . . . . . . . . . . . 13
|
58 | | ablgrp 18198 |
. . . . . . . . . . . . . . . 16
|
59 | 2 | grpbn0 17451 |
. . . . . . . . . . . . . . . 16
|
60 | 13, 58, 59 | 3syl 18 |
. . . . . . . . . . . . . . 15
|
61 | | hashnncl 13157 |
. . . . . . . . . . . . . . . 16
|
62 | 1, 61 | syl 17 |
. . . . . . . . . . . . . . 15
|
63 | 60, 62 | mpbird 247 |
. . . . . . . . . . . . . 14
|
64 | 63 | adantr 481 |
. . . . . . . . . . . . 13
|
65 | 57, 64 | pccld 15555 |
. . . . . . . . . . . 12
|
66 | 54, 65 | syldan 487 |
. . . . . . . . . . 11
|
67 | | pcdvdsb 15573 |
. . . . . . . . . . 11
DProd
DProd
DProd |
68 | 54, 56, 66, 67 | syl3anc 1326 |
. . . . . . . . . 10
DProd
DProd |
69 | 53, 68 | mpbird 247 |
. . . . . . . . 9
DProd |
70 | 69 | adantlr 751 |
. . . . . . . 8
DProd |
71 | 26, 70 | syldan 487 |
. . . . . . 7
DProd |
72 | | pceq0 15575 |
. . . . . . . . . 10
|
73 | 57, 64, 72 | syl2anc 693 |
. . . . . . . . 9
|
74 | 73 | biimpar 502 |
. . . . . . . 8
|
75 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
76 | 75 | subg0cl 17602 |
. . . . . . . . . . . . . 14
DProd SubGrp DProd |
77 | | ne0i 3921 |
. . . . . . . . . . . . . 14
DProd
DProd |
78 | 17, 76, 77 | 3syl 18 |
. . . . . . . . . . . . 13
DProd |
79 | | hashnncl 13157 |
. . . . . . . . . . . . . 14
DProd DProd
DProd |
80 | 6, 79 | syl 17 |
. . . . . . . . . . . . 13
DProd DProd |
81 | 78, 80 | mpbird 247 |
. . . . . . . . . . . 12
DProd |
82 | 81 | adantr 481 |
. . . . . . . . . . 11
DProd |
83 | 57, 82 | pccld 15555 |
. . . . . . . . . 10
DProd |
84 | 83 | nn0ge0d 11354 |
. . . . . . . . 9
DProd |
85 | 84 | adantr 481 |
. . . . . . . 8
DProd |
86 | 74, 85 | eqbrtrd 4675 |
. . . . . . 7
DProd |
87 | 71, 86 | pm2.61dan 832 |
. . . . . 6
DProd |
88 | 87 | ralrimiva 2966 |
. . . . 5
DProd |
89 | 10 | nn0zd 11480 |
. . . . . 6
|
90 | | pc2dvds 15583 |
. . . . . 6
DProd DProd
DProd |
91 | 89, 55, 90 | syl2anc 693 |
. . . . 5
DProd
DProd |
92 | 88, 91 | mpbird 247 |
. . . 4
DProd |
93 | | dvdseq 15036 |
. . . 4
DProd
DProd
DProd
DProd |
94 | 8, 10, 19, 92, 93 | syl22anc 1327 |
. . 3
DProd |
95 | | hashen 13135 |
. . . 4
DProd DProd DProd
|
96 | 6, 1, 95 | syl2anc 693 |
. . 3
DProd DProd
|
97 | 94, 96 | mpbid 222 |
. 2
DProd |
98 | | fisseneq 8171 |
. 2
DProd DProd
DProd |
99 | 1, 4, 97, 98 | syl3anc 1326 |
1
DProd |