Step | Hyp | Ref
| Expression |
1 | | nmzsubg.2 |
. . . . . 6
     |
2 | 1 | subgss 12965 |
. . . . 5
 SubGrp 
  |
3 | 2 | sselda 3155 |
. . . 4
  SubGrp     |
4 | | simpll 527 |
. . . . . . . 8
   SubGrp  
 
  
SubGrp    |
5 | | subgrcl 12970 |
. . . . . . . . . . . . 13
 SubGrp 
  |
6 | 4, 5 | syl 14 |
. . . . . . . . . . . 12
   SubGrp  
 
  
  |
7 | 4, 2 | syl 14 |
. . . . . . . . . . . . 13
   SubGrp  
 
  
  |
8 | | simplrl 535 |
. . . . . . . . . . . . 13
   SubGrp  
 
  
  |
9 | 7, 8 | sseldd 3156 |
. . . . . . . . . . . 12
   SubGrp  
 
  
  |
10 | | nmzsubg.3 |
. . . . . . . . . . . . 13
    |
11 | | eqid 2177 |
. . . . . . . . . . . . 13
         |
12 | | eqid 2177 |
. . . . . . . . . . . . 13
           |
13 | 1, 10, 11, 12 | grplinv 12854 |
. . . . . . . . . . . 12
 
                  |
14 | 6, 9, 13 | syl2anc 411 |
. . . . . . . . . . 11
   SubGrp  
 
  
         
       |
15 | 14 | oveq1d 5887 |
. . . . . . . . . 10
   SubGrp  
 
  
          
      
   |
16 | 12 | subginvcl 12974 |
. . . . . . . . . . . . 13
  SubGrp              |
17 | 4, 8, 16 | syl2anc 411 |
. . . . . . . . . . . 12
   SubGrp  
 
  
           |
18 | 7, 17 | sseldd 3156 |
. . . . . . . . . . 11
   SubGrp  
 
  
           |
19 | | simplrr 536 |
. . . . . . . . . . 11
   SubGrp  
 
  
  |
20 | 1, 10 | grpass 12818 |
. . . . . . . . . . 11
                                    
     |
21 | 6, 18, 9, 19, 20 | syl13anc 1240 |
. . . . . . . . . 10
   SubGrp  
 
  
          
           
     |
22 | 1, 10, 11 | grplid 12838 |
. . . . . . . . . . 11
 
         |
23 | 6, 19, 22 | syl2anc 411 |
. . . . . . . . . 10
   SubGrp  
 
  
        |
24 | 15, 21, 23 | 3eqtr3d 2218 |
. . . . . . . . 9
   SubGrp  
 
  
         
     |
25 | | simpr 110 |
. . . . . . . . . 10
   SubGrp  
 
  
    |
26 | 10 | subgcl 12975 |
. . . . . . . . . 10
  SubGrp                             |
27 | 4, 17, 25, 26 | syl3anc 1238 |
. . . . . . . . 9
   SubGrp  
 
  
         
     |
28 | 24, 27 | eqeltrrd 2255 |
. . . . . . . 8
   SubGrp  
 
  
  |
29 | 10 | subgcl 12975 |
. . . . . . . 8
  SubGrp 
 
   |
30 | 4, 28, 8, 29 | syl3anc 1238 |
. . . . . . 7
   SubGrp  
 
  
    |
31 | | simpll 527 |
. . . . . . . 8
   SubGrp  
 
  
SubGrp    |
32 | | simplrl 535 |
. . . . . . . 8
   SubGrp  
 
  
  |
33 | 31, 5 | syl 14 |
. . . . . . . . . 10
   SubGrp  
 
  
  |
34 | | simplrr 536 |
. . . . . . . . . 10
   SubGrp  
 
  
  |
35 | 31, 32, 3 | syl2anc 411 |
. . . . . . . . . 10
   SubGrp  
 
  
  |
36 | | eqid 2177 |
. . . . . . . . . . 11
         |
37 | 1, 10, 36 | grppncan 12893 |
. . . . . . . . . 10
 
             |
38 | 33, 34, 35, 37 | syl3anc 1238 |
. . . . . . . . 9
   SubGrp  
 
  
 
          |
39 | | simpr 110 |
. . . . . . . . . 10
   SubGrp  
 
  
    |
40 | 36 | subgsubcl 12976 |
. . . . . . . . . 10
  SubGrp  

             |
41 | 31, 39, 32, 40 | syl3anc 1238 |
. . . . . . . . 9
   SubGrp  
 
  
 
          |
42 | 38, 41 | eqeltrrd 2255 |
. . . . . . . 8
   SubGrp  
 
  
  |
43 | 10 | subgcl 12975 |
. . . . . . . 8
  SubGrp 
 
   |
44 | 31, 32, 42, 43 | syl3anc 1238 |
. . . . . . 7
   SubGrp  
 
  
    |
45 | 30, 44 | impbida 596 |
. . . . . 6
  SubGrp  
 
 

     |
46 | 45 | anassrs 400 |
. . . . 5
   SubGrp      
     |
47 | 46 | ralrimiva 2550 |
. . . 4
  SubGrp   
 

     |
48 | | elnmz.1 |
. . . . 5
          |
49 | 48 | elnmz 12999 |
. . . 4



 

      |
50 | 3, 47, 49 | sylanbrc 417 |
. . 3
  SubGrp     |
51 | 50 | ex 115 |
. 2
 SubGrp 

   |
52 | 51 | ssrdv 3161 |
1
 SubGrp 
  |