Step | Hyp | Ref
| Expression |
1 | | sylow2b.h |
. . . 4
SubGrp |
2 | | eqid 2622 |
. . . . 5
↾s ↾s |
3 | 2 | subggrp 17597 |
. . . 4
SubGrp
↾s |
4 | 1, 3 | syl 17 |
. . 3
↾s |
5 | | sylow2b.xf |
. . . . 5
|
6 | | pwfi 8261 |
. . . . 5
|
7 | 5, 6 | sylib 208 |
. . . 4
|
8 | | sylow2b.k |
. . . . . 6
SubGrp |
9 | | sylow2b.x |
. . . . . . 7
|
10 | | sylow2b.r |
. . . . . . 7
~QG |
11 | 9, 10 | eqger 17644 |
. . . . . 6
SubGrp
|
12 | 8, 11 | syl 17 |
. . . . 5
|
13 | 12 | qsss 7808 |
. . . 4
|
14 | 7, 13 | ssexd 4805 |
. . 3
|
15 | 4, 14 | jca 554 |
. 2
↾s |
16 | | sylow2b.m |
. . . . . . 7
|
17 | | vex 3203 |
. . . . . . . . 9
|
18 | 17 | mptex 6486 |
. . . . . . . 8
|
19 | 18 | rnex 7100 |
. . . . . . 7
|
20 | 16, 19 | fnmpt2i 7239 |
. . . . . 6
|
21 | 20 | a1i 11 |
. . . . 5
|
22 | | eqid 2622 |
. . . . . . . 8
|
23 | | oveq2 6658 |
. . . . . . . . 9
|
24 | 23 | eleq1d 2686 |
. . . . . . . 8
|
25 | | sylow2b.a |
. . . . . . . . . . 11
|
26 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 18035 |
. . . . . . . . . 10
|
27 | | ovex 6678 |
. . . . . . . . . . . 12
~QG |
28 | 10, 27 | eqeltri 2697 |
. . . . . . . . . . 11
|
29 | | subgrcl 17599 |
. . . . . . . . . . . . . 14
SubGrp
|
30 | 1, 29 | syl 17 |
. . . . . . . . . . . . 13
|
31 | 30 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
|
32 | 9 | subgss 17595 |
. . . . . . . . . . . . . . 15
SubGrp
|
33 | 1, 32 | syl 17 |
. . . . . . . . . . . . . 14
|
34 | 33 | sselda 3603 |
. . . . . . . . . . . . 13
|
35 | 34 | 3adant3 1081 |
. . . . . . . . . . . 12
|
36 | | simp3 1063 |
. . . . . . . . . . . 12
|
37 | 9, 25 | grpcl 17430 |
. . . . . . . . . . . 12
|
38 | 31, 35, 36, 37 | syl3anc 1326 |
. . . . . . . . . . 11
|
39 | | ecelqsg 7802 |
. . . . . . . . . . 11
|
40 | 28, 38, 39 | sylancr 695 |
. . . . . . . . . 10
|
41 | 26, 40 | eqeltrd 2701 |
. . . . . . . . 9
|
42 | 41 | 3expa 1265 |
. . . . . . . 8
|
43 | 22, 24, 42 | ectocld 7814 |
. . . . . . 7
|
44 | 43 | ralrimiva 2966 |
. . . . . 6
|
45 | 44 | ralrimiva 2966 |
. . . . 5
|
46 | | ffnov 6764 |
. . . . 5
|
47 | 21, 45, 46 | sylanbrc 698 |
. . . 4
|
48 | 2 | subgbas 17598 |
. . . . . . 7
SubGrp
↾s |
49 | 1, 48 | syl 17 |
. . . . . 6
↾s |
50 | 49 | xpeq1d 5138 |
. . . . 5
↾s |
51 | 50 | feq2d 6031 |
. . . 4
↾s |
52 | 47, 51 | mpbid 222 |
. . 3
↾s |
53 | | oveq2 6658 |
. . . . . . 7
↾s
↾s |
54 | | id 22 |
. . . . . . 7
|
55 | 53, 54 | eqeq12d 2637 |
. . . . . 6
↾s ↾s |
56 | | oveq2 6658 |
. . . . . . . 8
↾s ↾s |
57 | | oveq2 6658 |
. . . . . . . . 9
|
58 | 57 | oveq2d 6666 |
. . . . . . . 8
|
59 | 56, 58 | eqeq12d 2637 |
. . . . . . 7
↾s
↾s |
60 | 59 | 2ralbidv 2989 |
. . . . . 6
↾s
↾s
↾s
↾s
↾s
↾s |
61 | 55, 60 | anbi12d 747 |
. . . . 5
↾s ↾s ↾s
↾s
↾s
↾s
↾s
↾s |
62 | | simpl 473 |
. . . . . . . 8
|
63 | 1 | adantr 481 |
. . . . . . . . 9
SubGrp |
64 | | eqid 2622 |
. . . . . . . . . 10
|
65 | 64 | subg0cl 17602 |
. . . . . . . . 9
SubGrp
|
66 | 63, 65 | syl 17 |
. . . . . . . 8
|
67 | | simpr 477 |
. . . . . . . 8
|
68 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 18035 |
. . . . . . . 8
|
69 | 62, 66, 67, 68 | syl3anc 1326 |
. . . . . . 7
|
70 | 2, 64 | subg0 17600 |
. . . . . . . . 9
SubGrp
↾s |
71 | 63, 70 | syl 17 |
. . . . . . . 8
↾s |
72 | 71 | oveq1d 6665 |
. . . . . . 7
↾s |
73 | 9, 25, 64 | grplid 17452 |
. . . . . . . . 9
|
74 | 30, 73 | sylan 488 |
. . . . . . . 8
|
75 | 74 | eceq1d 7783 |
. . . . . . 7
|
76 | 69, 72, 75 | 3eqtr3d 2664 |
. . . . . 6
↾s |
77 | 63 | adantr 481 |
. . . . . . . . . . . . 13
SubGrp |
78 | 77, 29 | syl 17 |
. . . . . . . . . . . 12
|
79 | 77, 32 | syl 17 |
. . . . . . . . . . . . 13
|
80 | | simprl 794 |
. . . . . . . . . . . . 13
|
81 | 79, 80 | sseldd 3604 |
. . . . . . . . . . . 12
|
82 | | simprr 796 |
. . . . . . . . . . . . 13
|
83 | 79, 82 | sseldd 3604 |
. . . . . . . . . . . 12
|
84 | 67 | adantr 481 |
. . . . . . . . . . . 12
|
85 | 9, 25 | grpass 17431 |
. . . . . . . . . . . 12
|
86 | 78, 81, 83, 84, 85 | syl13anc 1328 |
. . . . . . . . . . 11
|
87 | 86 | eceq1d 7783 |
. . . . . . . . . 10
|
88 | 62 | adantr 481 |
. . . . . . . . . . 11
|
89 | 9, 25 | grpcl 17430 |
. . . . . . . . . . . 12
|
90 | 78, 83, 84, 89 | syl3anc 1326 |
. . . . . . . . . . 11
|
91 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 18035 |
. . . . . . . . . . 11
|
92 | 88, 80, 90, 91 | syl3anc 1326 |
. . . . . . . . . 10
|
93 | 87, 92 | eqtr4d 2659 |
. . . . . . . . 9
|
94 | 25 | subgcl 17604 |
. . . . . . . . . . 11
SubGrp
|
95 | 77, 80, 82, 94 | syl3anc 1326 |
. . . . . . . . . 10
|
96 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 18035 |
. . . . . . . . . 10
|
97 | 88, 95, 84, 96 | syl3anc 1326 |
. . . . . . . . 9
|
98 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 18035 |
. . . . . . . . . . 11
|
99 | 88, 82, 84, 98 | syl3anc 1326 |
. . . . . . . . . 10
|
100 | 99 | oveq2d 6666 |
. . . . . . . . 9
|
101 | 93, 97, 100 | 3eqtr4d 2666 |
. . . . . . . 8
|
102 | 101 | ralrimivva 2971 |
. . . . . . 7
|
103 | 63, 48 | syl 17 |
. . . . . . . 8
↾s |
104 | 2, 25 | ressplusg 15993 |
. . . . . . . . . . . . 13
SubGrp
↾s |
105 | 1, 104 | syl 17 |
. . . . . . . . . . . 12
↾s |
106 | 105 | oveqdr 6674 |
. . . . . . . . . . 11
↾s |
107 | 106 | oveq1d 6665 |
. . . . . . . . . 10
↾s |
108 | 107 | eqeq1d 2624 |
. . . . . . . . 9
↾s
|
109 | 103, 108 | raleqbidv 3152 |
. . . . . . . 8
↾s
↾s
|
110 | 103, 109 | raleqbidv 3152 |
. . . . . . 7
↾s
↾s
↾s
|
111 | 102, 110 | mpbid 222 |
. . . . . 6
↾s
↾s
↾s
|
112 | 76, 111 | jca 554 |
. . . . 5
↾s ↾s ↾s
↾s
|
113 | 22, 61, 112 | ectocld 7814 |
. . . 4
↾s ↾s
↾s
↾s |
114 | 113 | ralrimiva 2966 |
. . 3
↾s
↾s
↾s
↾s |
115 | 52, 114 | jca 554 |
. 2
↾s
↾s ↾s
↾s
↾s |
116 | | eqid 2622 |
. . 3
↾s ↾s |
117 | | eqid 2622 |
. . 3
↾s ↾s |
118 | | eqid 2622 |
. . 3
↾s ↾s |
119 | 116, 117,
118 | isga 17724 |
. 2
↾s
↾s
↾s
↾s ↾s
↾s
↾s |
120 | 15, 115, 119 | sylanbrc 698 |
1
↾s |