Step | Hyp | Ref
| Expression |
1 | | subrgsubg 13286 |
. . 3
 SubRing 
SubGrp    |
2 | | issubrg2.o |
. . . 4
     |
3 | 2 | subrg1cl 13288 |
. . 3
 SubRing 
  |
4 | | issubrg2.t |
. . . . . 6
     |
5 | 4 | subrgmcl 13292 |
. . . . 5
  SubRing 

    |
6 | 5 | 3expb 1204 |
. . . 4
  SubRing 

      |
7 | 6 | ralrimivva 2559 |
. . 3
 SubRing 


    |
8 | 1, 3, 7 | 3jca 1177 |
. 2
 SubRing 
 SubGrp   

    |
9 | | simpl 109 |
. . . 4
  
SubGrp 
        |
10 | | simpr1 1003 |
. . . . . 6
  
SubGrp 
      SubGrp    |
11 | | eqid 2177 |
. . . . . . 7
 ↾s   ↾s   |
12 | 11 | subgbas 12969 |
. . . . . 6
 SubGrp 
    ↾s     |
13 | 10, 12 | syl 14 |
. . . . 5
  
SubGrp 
          ↾s     |
14 | | eqidd 2178 |
. . . . . . 7
 SubGrp 
 ↾s   ↾s    |
15 | | eqidd 2178 |
. . . . . . 7
 SubGrp 
        |
16 | | id 19 |
. . . . . . 7
 SubGrp 
SubGrp    |
17 | | subgrcl 12970 |
. . . . . . 7
 SubGrp 
  |
18 | 14, 15, 16, 17 | ressplusgd 12579 |
. . . . . 6
 SubGrp 
      ↾s     |
19 | 10, 18 | syl 14 |
. . . . 5
  
SubGrp 
            ↾s     |
20 | 11, 4 | ressmulrg 12595 |
. . . . . 6
  SubGrp       ↾s     |
21 | 10, 17, 20 | syl2anc2 412 |
. . . . 5
  
SubGrp 
          ↾s     |
22 | 11 | subggrp 12968 |
. . . . . 6
 SubGrp 
 ↾s    |
23 | 10, 22 | syl 14 |
. . . . 5
  
SubGrp 
       ↾s    |
24 | | simpr3 1005 |
. . . . . . 7
  
SubGrp 
      

    |
25 | | oveq1 5879 |
. . . . . . . . 9
 
     |
26 | 25 | eleq1d 2246 |
. . . . . . . 8
   
     |
27 | | oveq2 5880 |
. . . . . . . . 9
 
     |
28 | 27 | eleq1d 2246 |
. . . . . . . 8
   
     |
29 | 26, 28 | rspc2v 2854 |
. . . . . . 7
 
           |
30 | 24, 29 | syl5com 29 |
. . . . . 6
  
SubGrp 
       

     |
31 | 30 | 3impib 1201 |
. . . . 5
    SubGrp 


   
 
   |
32 | | issubrg2.b |
. . . . . . . . . . 11
     |
33 | 32 | subgss 12965 |
. . . . . . . . . 10
 SubGrp 
  |
34 | 10, 33 | syl 14 |
. . . . . . . . 9
  
SubGrp 
        |
35 | 34 | sseld 3154 |
. . . . . . . 8
  
SubGrp 
      
   |
36 | 34 | sseld 3154 |
. . . . . . . 8
  
SubGrp 
          |
37 | 34 | sseld 3154 |
. . . . . . . 8
  
SubGrp 
      
   |
38 | 35, 36, 37 | 3anim123d 1319 |
. . . . . . 7
  
SubGrp 
       


    |
39 | 38 | imp 124 |
. . . . . 6
    SubGrp 


    
 

   |
40 | 32, 4 | ringass 13130 |
. . . . . . 7
  
 
 
        |
41 | 40 | adantlr 477 |
. . . . . 6
    SubGrp 


    
 
 
        |
42 | 39, 41 | syldan 282 |
. . . . 5
    SubGrp 


    
 
 
        |
43 | | eqid 2177 |
. . . . . . . 8
       |
44 | 32, 43, 4 | ringdi 13132 |
. . . . . . 7
  
 
                      |
45 | 44 | adantlr 477 |
. . . . . 6
    SubGrp 


    
 
                      |
46 | 39, 45 | syldan 282 |
. . . . 5
    SubGrp 


    
 
                      |
47 | 32, 43, 4 | ringdir 13133 |
. . . . . . 7
  
 
                      |
48 | 47 | adantlr 477 |
. . . . . 6
    SubGrp 


    
 
                      |
49 | 39, 48 | syldan 282 |
. . . . 5
    SubGrp 


    
 
                      |
50 | | simpr2 1004 |
. . . . 5
  
SubGrp 
        |
51 | 35 | imp 124 |
. . . . . 6
    SubGrp 


       |
52 | 32, 4, 2 | ringlidm 13137 |
. . . . . . 7
      |
53 | 52 | adantlr 477 |
. . . . . 6
    SubGrp 


        |
54 | 51, 53 | syldan 282 |
. . . . 5
    SubGrp 


        |
55 | 32, 4, 2 | ringridm 13138 |
. . . . . . 7
   
  |
56 | 55 | adantlr 477 |
. . . . . 6
    SubGrp 


     
  |
57 | 51, 56 | syldan 282 |
. . . . 5
    SubGrp 


     
  |
58 | 13, 19, 21, 23, 31, 42, 46, 49, 50, 54, 57 | isringd 13151 |
. . . 4
  
SubGrp 
       ↾s    |
59 | 34, 50 | jca 306 |
. . . 4
  
SubGrp 
          |
60 | 32, 2 | issubrg 13280 |
. . . 4
 SubRing   
 ↾s        |
61 | 9, 58, 59, 60 | syl21anbrc 1182 |
. . 3
  
SubGrp 
      SubRing    |
62 | 61 | ex 115 |
. 2

  SubGrp 


  
SubRing     |
63 | 8, 62 | impbid2 143 |
1

 SubRing   SubGrp   

     |