Step | Hyp | Ref
| Expression |
1 | | sylow3.xf |
. . . . . 6
   |
2 | | pwfi 7869 |
. . . . . 6

   |
3 | 1, 2 | sylib 200 |
. . . . 5
    |
4 | | slwsubg 17262 |
. . . . . . . 8
  pSyl 
SubGrp    |
5 | | sylow3.x |
. . . . . . . . 9
     |
6 | 5 | subgss 16818 |
. . . . . . . 8
 SubGrp 
  |
7 | 4, 6 | syl 17 |
. . . . . . 7
  pSyl 
  |
8 | | selpw 3958 |
. . . . . . 7
 
  |
9 | 7, 8 | sylibr 216 |
. . . . . 6
  pSyl 
   |
10 | 9 | ssriv 3436 |
. . . . 5
 pSyl    |
11 | | ssfi 7792 |
. . . . 5
    pSyl     pSyl
   |
12 | 3, 10, 11 | sylancl 668 |
. . . 4
  pSyl    |
13 | | hashcl 12538 |
. . . 4
  pSyl      pSyl     |
14 | 12, 13 | syl 17 |
. . 3
     pSyl     |
15 | 14 | nn0cnd 10927 |
. 2
     pSyl     |
16 | | sylow3.g |
. . . . . . 7
   |
17 | | sylow3lem2.n |
. . . . . . . 8
          |
18 | | sylow3lem1.a |
. . . . . . . 8
    |
19 | 17, 5, 18 | nmzsubg 16858 |
. . . . . . 7
 SubGrp    |
20 | | eqid 2451 |
. . . . . . . 8
 ~QG   ~QG   |
21 | 5, 20 | eqger 16867 |
. . . . . . 7
 SubGrp 
 ~QG    |
22 | 16, 19, 21 | 3syl 18 |
. . . . . 6
 
~QG    |
23 | 22 | qsss 7424 |
. . . . 5
     ~QG      |
24 | | ssfi 7792 |
. . . . 5
       ~QG         ~QG     |
25 | 3, 23, 24 | syl2anc 667 |
. . . 4
     ~QG     |
26 | | hashcl 12538 |
. . . 4
     ~QG          ~QG      |
27 | 25, 26 | syl 17 |
. . 3
        ~QG      |
28 | 27 | nn0cnd 10927 |
. 2
        ~QG      |
29 | 16, 19 | syl 17 |
. . . . 5
 SubGrp    |
30 | | eqid 2451 |
. . . . . 6
         |
31 | 30 | subg0cl 16825 |
. . . . 5
 SubGrp 
      |
32 | | ne0i 3737 |
. . . . 5
       |
33 | 29, 31, 32 | 3syl 18 |
. . . 4
   |
34 | 5 | subgss 16818 |
. . . . . . 7
 SubGrp 
  |
35 | 16, 19, 34 | 3syl 18 |
. . . . . 6

  |
36 | | ssfi 7792 |
. . . . . 6
  
  |
37 | 1, 35, 36 | syl2anc 667 |
. . . . 5
   |
38 | | hashnncl 12547 |
. . . . 5
     
   |
39 | 37, 38 | syl 17 |
. . . 4
     
   |
40 | 33, 39 | mpbird 236 |
. . 3
       |
41 | 40 | nncnd 10625 |
. 2
       |
42 | 40 | nnne0d 10654 |
. 2
       |
43 | | sylow3.p |
. . . . 5
   |
44 | | sylow3lem1.d |
. . . . 5
     |
45 | | sylow3lem1.m |
. . . . 5
   pSyl     
    |
46 | 5, 16, 1, 43, 18, 44, 45 | sylow3lem1 17279 |
. . . 4

 
pSyl     |
47 | | sylow3lem2.k |
. . . 4
  pSyl    |
48 | | sylow3lem2.h |
. . . . 5
     |
49 | | eqid 2451 |
. . . . 5
 ~QG   ~QG   |
50 | | eqid 2451 |
. . . . 5
       
 pSyl  
            
pSyl        |
51 | 5, 48, 49, 50 | orbsta2 16968 |
. . . 4
 
  pSyl    pSyl              ![] ]](rbrack.gif)        
 pSyl  
            |
52 | 46, 47, 1, 51 | syl21anc 1267 |
. . 3
           ![] ]](rbrack.gif)    
     pSyl 

            |
53 | 5, 20, 29, 1 | lagsubg2 16878 |
. . 3
            
~QG           |
54 | 50, 5 | gaorber 16962 |
. . . . . . . 8
  pSyl      
     pSyl 

     pSyl    |
55 | 46, 54 | syl 17 |
. . . . . . 7
    
     pSyl 

     pSyl    |
56 | 55 | ecss 7405 |
. . . . . 6
   ![] ]](rbrack.gif)         
pSyl        pSyl    |
57 | 47 | adantr 467 |
. . . . . . . . . 10
 

pSyl  

pSyl    |
58 | | simpr 463 |
. . . . . . . . . 10
 

pSyl  

pSyl    |
59 | 1 | adantr 467 |
. . . . . . . . . . . 12
 

pSyl  
  |
60 | 5, 59, 58, 57, 18, 44 | sylow2 17278 |
. . . . . . . . . . 11
 

pSyl  

        |
61 | | eqcom 2458 |
. . . . . . . . . . . . 13
 

    |
62 | | simpr 463 |
. . . . . . . . . . . . . . 15
    pSyl      |
63 | 57 | adantr 467 |
. . . . . . . . . . . . . . 15
    pSyl     pSyl    |
64 | | mptexg 6135 |
. . . . . . . . . . . . . . . 16
  pSyl 

       |
65 | | rnexg 6725 |
. . . . . . . . . . . . . . . 16
    
          |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . . . . . . . . . 15
    pSyl            |
67 | | simpr 463 |
. . . . . . . . . . . . . . . . . 18
 
   |
68 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
69 | 68 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . 19
 
       |
70 | 69, 68 | oveq12d 6308 |
. . . . . . . . . . . . . . . . . 18
 
           |
71 | 67, 70 | mpteq12dv 4481 |
. . . . . . . . . . . . . . . . 17
 
          
    |
72 | 71 | rneqd 5062 |
. . . . . . . . . . . . . . . 16
 
               |
73 | 72, 45 | ovmpt2ga 6426 |
. . . . . . . . . . . . . . 15
 
 pSyl     
             |
74 | 62, 63, 66, 73 | syl3anc 1268 |
. . . . . . . . . . . . . 14
    pSyl              |
75 | 74 | eqeq2d 2461 |
. . . . . . . . . . . . 13
    pSyl      
         |
76 | 61, 75 | syl5bb 261 |
. . . . . . . . . . . 12
    pSyl      
         |
77 | 76 | rexbidva 2898 |
. . . . . . . . . . 11
 

pSyl  
 
  
         |
78 | 60, 77 | mpbird 236 |
. . . . . . . . . 10
 

pSyl  

    |
79 | 50 | gaorb 16961 |
. . . . . . . . . 10
     
     pSyl 

    
  pSyl   pSyl   
    |
80 | 57, 58, 78, 79 | syl3anbrc 1192 |
. . . . . . . . 9
 

pSyl  
         
pSyl          |
81 | | elecg 7402 |
. . . . . . . . . 10
   pSyl   pSyl  
   ![] ]](rbrack.gif)         
pSyl               
 pSyl  
        |
82 | 58, 57, 81 | syl2anc 667 |
. . . . . . . . 9
 

pSyl  
   ![] ]](rbrack.gif)         
pSyl               
 pSyl  
        |
83 | 80, 82 | mpbird 236 |
. . . . . . . 8
 

pSyl  
  ![] ]](rbrack.gif)        
 pSyl  
      |
84 | 83 | ex 436 |
. . . . . . 7
   pSyl 
  ![] ]](rbrack.gif)    
     pSyl 

       |
85 | 84 | ssrdv 3438 |
. . . . . 6
  pSyl    ![] ]](rbrack.gif)    
     pSyl 

      |
86 | 56, 85 | eqssd 3449 |
. . . . 5
   ![] ]](rbrack.gif)         
pSyl        pSyl    |
87 | 86 | fveq2d 5869 |
. . . 4
      ![] ]](rbrack.gif)        
 pSyl  
         pSyl     |
88 | 5, 16, 1, 43, 18, 44, 45, 47, 48, 17 | sylow3lem2 17280 |
. . . . 5
   |
89 | 88 | fveq2d 5869 |
. . . 4
           |
90 | 87, 89 | oveq12d 6308 |
. . 3
       ![] ]](rbrack.gif)        
 pSyl  
               pSyl          |
91 | 52, 53, 90 | 3eqtr3rd 2494 |
. 2
      pSyl                ~QG           |
92 | 15, 28, 41, 42, 91 | mulcan2ad 10248 |
1
     pSyl          ~QG      |