Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . . 4
pSyl pSyl |
2 | | slwsubg 18025 |
. . . 4
pSyl
SubGrp |
3 | 1, 2 | syl 17 |
. . 3
pSyl SubGrp |
4 | | fislw.1 |
. . . 4
|
5 | | simpl2 1065 |
. . . 4
pSyl |
6 | 4, 5, 1 | slwhash 18039 |
. . 3
pSyl |
7 | 3, 6 | jca 554 |
. 2
pSyl
SubGrp
|
8 | | simpl3 1066 |
. . 3
SubGrp
|
9 | | simprl 794 |
. . 3
SubGrp
SubGrp |
10 | | simpl2 1065 |
. . . . . . . . 9
SubGrp
|
11 | 10 | adantr 481 |
. . . . . . . 8
SubGrp SubGrp
pGrp ↾s |
12 | | simprl 794 |
. . . . . . . . 9
SubGrp SubGrp
pGrp ↾s SubGrp |
13 | 4 | subgss 17595 |
. . . . . . . . 9
SubGrp
|
14 | 12, 13 | syl 17 |
. . . . . . . 8
SubGrp SubGrp
pGrp ↾s |
15 | | ssfi 8180 |
. . . . . . . 8
|
16 | 11, 14, 15 | syl2anc 693 |
. . . . . . 7
SubGrp SubGrp
pGrp ↾s |
17 | | simprrl 804 |
. . . . . . 7
SubGrp SubGrp
pGrp ↾s |
18 | | ssdomg 8001 |
. . . . . . . . 9
|
19 | 16, 17, 18 | sylc 65 |
. . . . . . . 8
SubGrp SubGrp
pGrp ↾s |
20 | | simprrr 805 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
pGrp ↾s pGrp
↾s |
21 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
↾s ↾s |
22 | 21 | subggrp 17597 |
. . . . . . . . . . . . . . . . 17
SubGrp
↾s |
23 | 12, 22 | syl 17 |
. . . . . . . . . . . . . . . 16
SubGrp SubGrp
pGrp ↾s ↾s |
24 | 21 | subgbas 17598 |
. . . . . . . . . . . . . . . . . 18
SubGrp
↾s |
25 | 12, 24 | syl 17 |
. . . . . . . . . . . . . . . . 17
SubGrp SubGrp
pGrp ↾s ↾s |
26 | 25, 16 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . 16
SubGrp SubGrp
pGrp ↾s ↾s |
27 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
↾s ↾s |
28 | 27 | pgpfi 18020 |
. . . . . . . . . . . . . . . 16
↾s
↾s pGrp
↾s ↾s |
29 | 23, 26, 28 | syl2anc 693 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
pGrp ↾s pGrp ↾s
↾s |
30 | 20, 29 | mpbid 222 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
pGrp ↾s ↾s |
31 | 30 | simpld 475 |
. . . . . . . . . . . . 13
SubGrp SubGrp
pGrp ↾s |
32 | | prmnn 15388 |
. . . . . . . . . . . . 13
|
33 | 31, 32 | syl 17 |
. . . . . . . . . . . 12
SubGrp SubGrp
pGrp ↾s |
34 | 33 | nnred 11035 |
. . . . . . . . . . 11
SubGrp SubGrp
pGrp ↾s |
35 | 33 | nnge1d 11063 |
. . . . . . . . . . 11
SubGrp SubGrp
pGrp ↾s |
36 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
37 | 36 | subg0cl 17602 |
. . . . . . . . . . . . . . . . 17
SubGrp
|
38 | 12, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
SubGrp SubGrp
pGrp ↾s |
39 | | ne0i 3921 |
. . . . . . . . . . . . . . . 16
|
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
pGrp ↾s |
41 | | hashnncl 13157 |
. . . . . . . . . . . . . . . 16
|
42 | 16, 41 | syl 17 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
pGrp ↾s |
43 | 40, 42 | mpbird 247 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
pGrp ↾s |
44 | 31, 43 | pccld 15555 |
. . . . . . . . . . . . 13
SubGrp SubGrp
pGrp ↾s |
45 | 44 | nn0zd 11480 |
. . . . . . . . . . . 12
SubGrp SubGrp
pGrp ↾s |
46 | | simpl1 1064 |
. . . . . . . . . . . . . . . . 17
SubGrp
|
47 | 4 | grpbn0 17451 |
. . . . . . . . . . . . . . . . 17
|
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . . 16
SubGrp
|
49 | | hashnncl 13157 |
. . . . . . . . . . . . . . . . 17
|
50 | 10, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
SubGrp
|
51 | 48, 50 | mpbird 247 |
. . . . . . . . . . . . . . 15
SubGrp
|
52 | 8, 51 | pccld 15555 |
. . . . . . . . . . . . . 14
SubGrp
|
53 | 52 | adantr 481 |
. . . . . . . . . . . . 13
SubGrp SubGrp
pGrp ↾s |
54 | 53 | nn0zd 11480 |
. . . . . . . . . . . 12
SubGrp SubGrp
pGrp ↾s |
55 | 4 | lagsubg 17656 |
. . . . . . . . . . . . . . 15
SubGrp |
56 | 12, 11, 55 | syl2anc 693 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
pGrp ↾s
|
57 | 43 | nnzd 11481 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
pGrp ↾s |
58 | 51 | adantr 481 |
. . . . . . . . . . . . . . . 16
SubGrp SubGrp
pGrp ↾s |
59 | 58 | nnzd 11481 |
. . . . . . . . . . . . . . 15
SubGrp SubGrp
pGrp ↾s |
60 | | pc2dvds 15583 |
. . . . . . . . . . . . . . 15
|
61 | 57, 59, 60 | syl2anc 693 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
pGrp ↾s
|
62 | 56, 61 | mpbid 222 |
. . . . . . . . . . . . 13
SubGrp SubGrp
pGrp ↾s
|
63 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
64 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
65 | 63, 64 | breq12d 4666 |
. . . . . . . . . . . . . 14
|
66 | 65 | rspcv 3305 |
. . . . . . . . . . . . 13
|
67 | 31, 62, 66 | sylc 65 |
. . . . . . . . . . . 12
SubGrp SubGrp
pGrp ↾s
|
68 | | eluz2 11693 |
. . . . . . . . . . . 12
|
69 | 45, 54, 67, 68 | syl3anbrc 1246 |
. . . . . . . . . . 11
SubGrp SubGrp
pGrp ↾s
|
70 | 34, 35, 69 | leexp2ad 13041 |
. . . . . . . . . 10
SubGrp SubGrp
pGrp ↾s
|
71 | 30 | simprd 479 |
. . . . . . . . . . . 12
SubGrp SubGrp
pGrp ↾s
↾s |
72 | 25 | fveq2d 6195 |
. . . . . . . . . . . . . 14
SubGrp SubGrp
pGrp ↾s ↾s |
73 | 72 | eqeq1d 2624 |
. . . . . . . . . . . . 13
SubGrp SubGrp
pGrp ↾s
↾s |
74 | 73 | rexbidv 3052 |
. . . . . . . . . . . 12
SubGrp SubGrp
pGrp ↾s
↾s |
75 | 71, 74 | mpbird 247 |
. . . . . . . . . . 11
SubGrp SubGrp
pGrp ↾s |
76 | | pcprmpw 15587 |
. . . . . . . . . . . 12
|
77 | 31, 43, 76 | syl2anc 693 |
. . . . . . . . . . 11
SubGrp SubGrp
pGrp ↾s
|
78 | 75, 77 | mpbid 222 |
. . . . . . . . . 10
SubGrp SubGrp
pGrp ↾s |
79 | | simplrr 801 |
. . . . . . . . . 10
SubGrp SubGrp
pGrp ↾s |
80 | 70, 78, 79 | 3brtr4d 4685 |
. . . . . . . . 9
SubGrp SubGrp
pGrp ↾s
|
81 | 4 | subgss 17595 |
. . . . . . . . . . . . 13
SubGrp
|
82 | 81 | ad2antrl 764 |
. . . . . . . . . . . 12
SubGrp
|
83 | | ssfi 8180 |
. . . . . . . . . . . 12
|
84 | 10, 82, 83 | syl2anc 693 |
. . . . . . . . . . 11
SubGrp
|
85 | 84 | adantr 481 |
. . . . . . . . . 10
SubGrp SubGrp
pGrp ↾s |
86 | | hashdom 13168 |
. . . . . . . . . 10
|
87 | 16, 85, 86 | syl2anc 693 |
. . . . . . . . 9
SubGrp SubGrp
pGrp ↾s
|
88 | 80, 87 | mpbid 222 |
. . . . . . . 8
SubGrp SubGrp
pGrp ↾s |
89 | | sbth 8080 |
. . . . . . . 8
|
90 | 19, 88, 89 | syl2anc 693 |
. . . . . . 7
SubGrp SubGrp
pGrp ↾s |
91 | | fisseneq 8171 |
. . . . . . 7
|
92 | 16, 17, 90, 91 | syl3anc 1326 |
. . . . . 6
SubGrp SubGrp
pGrp ↾s |
93 | 92 | expr 643 |
. . . . 5
SubGrp SubGrp pGrp ↾s |
94 | | eqid 2622 |
. . . . . . . . . . . . 13
↾s ↾s |
95 | 94 | subgbas 17598 |
. . . . . . . . . . . 12
SubGrp
↾s |
96 | 95 | ad2antrl 764 |
. . . . . . . . . . 11
SubGrp
↾s |
97 | 96 | fveq2d 6195 |
. . . . . . . . . 10
SubGrp
↾s |
98 | | simprr 796 |
. . . . . . . . . 10
SubGrp
|
99 | 97, 98 | eqtr3d 2658 |
. . . . . . . . 9
SubGrp
↾s |
100 | | oveq2 6658 |
. . . . . . . . . . 11
|
101 | 100 | eqeq2d 2632 |
. . . . . . . . . 10
↾s
↾s |
102 | 101 | rspcev 3309 |
. . . . . . . . 9
↾s ↾s |
103 | 52, 99, 102 | syl2anc 693 |
. . . . . . . 8
SubGrp
↾s |
104 | 94 | subggrp 17597 |
. . . . . . . . . 10
SubGrp
↾s |
105 | 104 | ad2antrl 764 |
. . . . . . . . 9
SubGrp
↾s |
106 | 96, 84 | eqeltrrd 2702 |
. . . . . . . . 9
SubGrp
↾s |
107 | | eqid 2622 |
. . . . . . . . . 10
↾s ↾s |
108 | 107 | pgpfi 18020 |
. . . . . . . . 9
↾s ↾s pGrp
↾s
↾s |
109 | 105, 106,
108 | syl2anc 693 |
. . . . . . . 8
SubGrp
pGrp
↾s
↾s |
110 | 8, 103, 109 | mpbir2and 957 |
. . . . . . 7
SubGrp
pGrp ↾s |
111 | 110 | adantr 481 |
. . . . . 6
SubGrp SubGrp pGrp
↾s |
112 | | oveq2 6658 |
. . . . . . . 8
↾s ↾s |
113 | 112 | breq2d 4665 |
. . . . . . 7
pGrp
↾s
pGrp ↾s |
114 | | eqimss 3657 |
. . . . . . . 8
|
115 | 114 | biantrurd 529 |
. . . . . . 7
pGrp
↾s
pGrp ↾s |
116 | 113, 115 | bitrd 268 |
. . . . . 6
pGrp
↾s
pGrp ↾s |
117 | 111, 116 | syl5ibcom 235 |
. . . . 5
SubGrp SubGrp pGrp ↾s |
118 | 93, 117 | impbid 202 |
. . . 4
SubGrp SubGrp pGrp ↾s
|
119 | 118 | ralrimiva 2966 |
. . 3
SubGrp
SubGrp pGrp ↾s
|
120 | | isslw 18023 |
. . 3
pSyl SubGrp
SubGrp pGrp
↾s |
121 | 8, 9, 119, 120 | syl3anbrc 1246 |
. 2
SubGrp
pSyl |
122 | 7, 121 | impbida 877 |
1
pSyl SubGrp |