Step | Hyp | Ref
| Expression |
1 | | sylow2b.h |
. . . 4
 SubGrp    |
2 | | eqid 2471 |
. . . . 5
 ↾s   ↾s   |
3 | 2 | subggrp 16898 |
. . . 4
 SubGrp 
 ↾s    |
4 | 1, 3 | syl 17 |
. . 3
 
↾s    |
5 | | sylow2b.xf |
. . . . 5
   |
6 | | pwfi 7887 |
. . . . 5

   |
7 | 5, 6 | sylib 201 |
. . . 4
    |
8 | | sylow2b.k |
. . . . . 6
 SubGrp    |
9 | | sylow2b.x |
. . . . . . 7
     |
10 | | sylow2b.r |
. . . . . . 7

~QG   |
11 | 9, 10 | eqger 16945 |
. . . . . 6
 SubGrp 
  |
12 | 8, 11 | syl 17 |
. . . . 5
   |
13 | 12 | qsss 7442 |
. . . 4
      |
14 | 7, 13 | ssexd 4543 |
. . 3
  
  |
15 | 4, 14 | jca 541 |
. 2
   ↾s       |
16 | | sylow2b.m |
. . . . . . 7


        |
17 | | vex 3034 |
. . . . . . . . 9
 |
18 | 17 | mptex 6152 |
. . . . . . . 8
     |
19 | 18 | rnex 6746 |
. . . . . . 7
     |
20 | 16, 19 | fnmpt2i 6881 |
. . . . . 6

    |
21 | 20 | a1i 11 |
. . . . 5
       |
22 | | eqid 2471 |
. . . . . . . 8
     |
23 | | oveq2 6316 |
. . . . . . . . 9
          |
24 | 23 | eleq1d 2533 |
. . . . . . . 8
      
 
       |
25 | | sylow2b.a |
. . . . . . . . . . 11
    |
26 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 17350 |
. . . . . . . . . 10
 

  
 
   |
27 | | ovex 6336 |
. . . . . . . . . . . 12
 ~QG   |
28 | 10, 27 | eqeltri 2545 |
. . . . . . . . . . 11
 |
29 | | subgrcl 16900 |
. . . . . . . . . . . . . 14
 SubGrp 
  |
30 | 1, 29 | syl 17 |
. . . . . . . . . . . . 13
   |
31 | 30 | 3ad2ant1 1051 |
. . . . . . . . . . . 12
 

  |
32 | 9 | subgss 16896 |
. . . . . . . . . . . . . . 15
 SubGrp 
  |
33 | 1, 32 | syl 17 |
. . . . . . . . . . . . . 14

  |
34 | 33 | sselda 3418 |
. . . . . . . . . . . . 13
 
   |
35 | 34 | 3adant3 1050 |
. . . . . . . . . . . 12
 

  |
36 | | simp3 1032 |
. . . . . . . . . . . 12
 

  |
37 | 9, 25 | grpcl 16757 |
. . . . . . . . . . . 12
 
     |
38 | 31, 35, 36, 37 | syl3anc 1292 |
. . . . . . . . . . 11
 

    |
39 | | ecelqsg 7436 |
. . . . . . . . . . 11
 
          |
40 | 28, 38, 39 | sylancr 676 |
. . . . . . . . . 10
 

 
      |
41 | 26, 40 | eqeltrd 2549 |
. . . . . . . . 9
 

  
    |
42 | 41 | 3expa 1231 |
. . . . . . . 8
     
      |
43 | 22, 24, 42 | ectocld 7448 |
. . . . . . 7
       
     |
44 | 43 | ralrimiva 2809 |
. . . . . 6
 
           |
45 | 44 | ralrimiva 2809 |
. . . . 5
  
         |
46 | | ffnov 6419 |
. . . . 5
             

          |
47 | 21, 45, 46 | sylanbrc 677 |
. . . 4
            |
48 | 2 | subgbas 16899 |
. . . . . . 7
 SubGrp 
    ↾s     |
49 | 1, 48 | syl 17 |
. . . . . 6
    
↾s     |
50 | 49 | xpeq1d 4862 |
. . . . 5
         
↾s        |
51 | 50 | feq2d 5725 |
. . . 4
               
↾s             |
52 | 47, 51 | mpbid 215 |
. . 3
       ↾s            |
53 | | oveq2 6316 |
. . . . . . 7
        ↾s         
↾s      |
54 | | id 22 |
. . . . . . 7
       |
55 | 53, 54 | eqeq12d 2486 |
. . . . . 6
         ↾s            ↾s       |
56 | | oveq2 6316 |
. . . . . . . 8
         ↾s             ↾s        |
57 | | oveq2 6316 |
. . . . . . . . 9
          |
58 | 57 | oveq2d 6324 |
. . . . . . . 8
              |
59 | 56, 58 | eqeq12d 2486 |
. . . . . . 7
          ↾s        
  
      ↾s             |
60 | 59 | 2ralbidv 2832 |
. . . . . 6
         ↾s    
   
↾s         
↾s        
  
     ↾s    
   
↾s         
↾s             |
61 | 55, 60 | anbi12d 725 |
. . . . 5
          ↾s            ↾s         ↾s         
↾s        
          ↾s    
   
↾s    
   
↾s         
↾s              |
62 | | simpl 464 |
. . . . . . . 8
 
   |
63 | 1 | adantr 472 |
. . . . . . . . 9
 
 SubGrp    |
64 | | eqid 2471 |
. . . . . . . . . 10
         |
65 | 64 | subg0cl 16903 |
. . . . . . . . 9
 SubGrp 
      |
66 | 63, 65 | syl 17 |
. . . . . . . 8
 
       |
67 | | simpr 468 |
. . . . . . . 8
 
   |
68 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 17350 |
. . . . . . . 8
 
   

                |
69 | 62, 66, 67, 68 | syl3anc 1292 |
. . . . . . 7
 
     
           |
70 | 2, 64 | subg0 16901 |
. . . . . . . . 9
 SubGrp 
        ↾s     |
71 | 63, 70 | syl 17 |
. . . . . . . 8
 
         ↾s     |
72 | 71 | oveq1d 6323 |
. . . . . . 7
 
     
       ↾s       |
73 | 9, 25, 64 | grplid 16774 |
. . . . . . . . 9
 
         |
74 | 30, 73 | sylan 479 |
. . . . . . . 8
 
     
   |
75 | 74 | eceq1d 7418 |
. . . . . . 7
 
      
     |
76 | 69, 72, 75 | 3eqtr3d 2513 |
. . . . . 6
 
      ↾s        |
77 | 63 | adantr 472 |
. . . . . . . . . . . . 13
    
 
SubGrp    |
78 | 77, 29 | syl 17 |
. . . . . . . . . . . 12
    
 
  |
79 | 77, 32 | syl 17 |
. . . . . . . . . . . . 13
    
 
  |
80 | | simprl 772 |
. . . . . . . . . . . . 13
    
 
  |
81 | 79, 80 | sseldd 3419 |
. . . . . . . . . . . 12
    
 
  |
82 | | simprr 774 |
. . . . . . . . . . . . 13
    
 
  |
83 | 79, 82 | sseldd 3419 |
. . . . . . . . . . . 12
    
 
  |
84 | 67 | adantr 472 |
. . . . . . . . . . . 12
    
 
  |
85 | 9, 25 | grpass 16758 |
. . . . . . . . . . . 12
  
    
       |
86 | 78, 81, 83, 84, 85 | syl13anc 1294 |
. . . . . . . . . . 11
    
 
 
        |
87 | 86 | eceq1d 7418 |
. . . . . . . . . 10
    
 
   
         |
88 | 62 | adantr 472 |
. . . . . . . . . . 11
    
 
  |
89 | 9, 25 | grpcl 16757 |
. . . . . . . . . . . 12
 
     |
90 | 78, 83, 84, 89 | syl3anc 1292 |
. . . . . . . . . . 11
    
 
    |
91 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 17350 |
. . . . . . . . . . 11
 
  
    
 
     |
92 | 88, 80, 90, 91 | syl3anc 1292 |
. . . . . . . . . 10
    
 
    
 
     |
93 | 87, 92 | eqtr4d 2508 |
. . . . . . . . 9
    
 
   
         |
94 | 25 | subgcl 16905 |
. . . . . . . . . . 11
  SubGrp 
 
   |
95 | 77, 80, 82, 94 | syl3anc 1292 |
. . . . . . . . . 10
    
 
    |
96 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 17350 |
. . . . . . . . . 10
 
 

 
  
   
   |
97 | 88, 95, 84, 96 | syl3anc 1292 |
. . . . . . . . 9
    
 
 
  
   
   |
98 | 9, 5, 1, 8, 25, 10, 16 | sylow2blem1 17350 |
. . . . . . . . . . 11
 

  
 
   |
99 | 88, 82, 84, 98 | syl3anc 1292 |
. . . . . . . . . 10
    
 
  
 
   |
100 | 99 | oveq2d 6324 |
. . . . . . . . 9
    
 
            |
101 | 93, 97, 100 | 3eqtr4d 2515 |
. . . . . . . 8
    
 
 
  
       |
102 | 101 | ralrimivva 2814 |
. . . . . . 7
 
 

 
  
       |
103 | 63, 48 | syl 17 |
. . . . . . . 8
 
     ↾s     |
104 | 2, 25 | ressplusg 15317 |
. . . . . . . . . . . . 13
 SubGrp 
   ↾s     |
105 | 1, 104 | syl 17 |
. . . . . . . . . . . 12
   
↾s     |
106 | 105 | oveqdr 6332 |
. . . . . . . . . . 11
 
 
      ↾s       |
107 | 106 | oveq1d 6323 |
. . . . . . . . . 10
 
   
       
↾s         |
108 | 107 | eqeq1d 2473 |
. . . . . . . . 9
 
        
  
      ↾s        
      |
109 | 103, 108 | raleqbidv 2987 |
. . . . . . . 8
 
  
      
  
     ↾s         
↾s        
      |
110 | 103, 109 | raleqbidv 2987 |
. . . . . . 7
 
  

      
  
     ↾s    
   
↾s         
↾s        
      |
111 | 102, 110 | mpbid 215 |
. . . . . 6
 
      ↾s    
   
↾s         
↾s        
     |
112 | 76, 111 | jca 541 |
. . . . 5
 
      
↾s            ↾s         ↾s         
↾s        
      |
113 | 22, 61, 112 | ectocld 7448 |
. . . 4
 
  
      ↾s         ↾s    
   
↾s         
↾s             |
114 | 113 | ralrimiva 2809 |
. . 3
           ↾s    
   
↾s    
   
↾s         
↾s             |
115 | 52, 114 | jca 541 |
. 2
       ↾s                   
↾s         ↾s    
   
↾s         
↾s              |
116 | | eqid 2471 |
. . 3
   
↾s       ↾s    |
117 | | eqid 2471 |
. . 3
  
↾s      ↾s    |
118 | | eqid 2471 |
. . 3
    ↾s       ↾s    |
119 | 116, 117,
118 | isga 17023 |
. 2
  ↾s    
  
↾s   

      ↾s                   
↾s         ↾s    
   
↾s         
↾s               |
120 | 15, 115, 119 | sylanbrc 677 |
1
   ↾s       |