Proof of Theorem resrhm2b
| Step | Hyp | Ref
 | Expression | 
| 1 |   | subrgsubg 13783 | 
. . . . . 6
        SubRing     
     SubGrp     | 
| 2 |   | resrhm2b.u | 
. . . . . . 7
        
↾s    | 
| 3 | 2 | resghm2b 13392 | 
. . . . . 6
         SubGrp                               
      
       | 
| 4 | 1, 3 | sylan 283 | 
. . . . 5
         SubRing     
               
         
      
       | 
| 5 |   | eqid 2196 | 
. . . . . . . 8
   mulGrp       mulGrp    | 
| 6 | 5 | subrgsubm 13790 | 
. . . . . . 7
        SubRing     
     SubMnd  mulGrp      | 
| 7 |   | eqid 2196 | 
. . . . . . . 8
    mulGrp   
↾s        mulGrp    ↾s    | 
| 8 | 7 | resmhm2b 13121 | 
. . . . . . 7
         SubMnd  mulGrp                      
  mulGrp    MndHom  mulGrp      
      mulGrp    MndHom   mulGrp    ↾s       | 
| 9 | 6, 8 | sylan 283 | 
. . . . . 6
         SubRing     
               
  mulGrp    MndHom  mulGrp      
      mulGrp    MndHom   mulGrp    ↾s       | 
| 10 |   | subrgrcl 13782 | 
. . . . . . . . . 10
        SubRing     
       | 
| 11 | 2, 5 | mgpress 13487 | 
. . . . . . . . . 10
                 SubRing      
  mulGrp   
↾s       mulGrp     | 
| 12 | 10, 11 | mpancom 422 | 
. . . . . . . . 9
        SubRing     
  mulGrp   
↾s       mulGrp     | 
| 13 | 12 | adantr 276 | 
. . . . . . . 8
         SubRing     
             mulGrp    ↾s       mulGrp     | 
| 14 | 13 | oveq2d 5938 | 
. . . . . . 7
         SubRing     
             mulGrp    MndHom   mulGrp    ↾s         mulGrp    MndHom  mulGrp      | 
| 15 | 14 | eleq2d 2266 | 
. . . . . 6
         SubRing     
               
  mulGrp    MndHom   mulGrp   
↾s      
      mulGrp    MndHom  mulGrp       | 
| 16 | 9, 15 | bitrd 188 | 
. . . . 5
         SubRing     
               
  mulGrp    MndHom  mulGrp      
      mulGrp    MndHom  mulGrp       | 
| 17 | 4, 16 | anbi12d 473 | 
. . . 4
         SubRing     
                              
  mulGrp    MndHom  mulGrp                          
  mulGrp    MndHom  mulGrp        | 
| 18 | 17 | anbi2d 464 | 
. . 3
         SubRing     
                                       
  mulGrp    MndHom  mulGrp                                       mulGrp    MndHom  mulGrp         | 
| 19 | 10 | adantr 276 | 
. . . . 5
         SubRing     
                  | 
| 20 | 19 | biantrud 304 | 
. . . 4
         SubRing     
               
   
        
         | 
| 21 | 20 | anbi1d 465 | 
. . 3
         SubRing     
                                       
  mulGrp    MndHom  mulGrp                
               
                mulGrp    MndHom  mulGrp         | 
| 22 | 2 | subrgring 13780 | 
. . . . . 6
        SubRing     
       | 
| 23 | 22 | adantr 276 | 
. . . . 5
         SubRing     
                  | 
| 24 | 23 | biantrud 304 | 
. . . 4
         SubRing     
               
   
        
         | 
| 25 | 24 | anbi1d 465 | 
. . 3
         SubRing     
                                       
  mulGrp    MndHom  mulGrp                
               
                mulGrp    MndHom  mulGrp         | 
| 26 | 18, 21, 25 | 3bitr3d 218 | 
. 2
         SubRing     
                                                    mulGrp    MndHom  mulGrp                
               
                mulGrp    MndHom  mulGrp         | 
| 27 |   | eqid 2196 | 
. . 3
   mulGrp       mulGrp    | 
| 28 | 27, 5 | isrhm 13714 | 
. 2
          RingHom             
               
                mulGrp    MndHom  mulGrp        | 
| 29 |   | eqid 2196 | 
. . 3
   mulGrp       mulGrp    | 
| 30 | 27, 29 | isrhm 13714 | 
. 2
          RingHom             
               
                mulGrp    MndHom  mulGrp        | 
| 31 | 26, 28, 30 | 3bitr4g 223 | 
1
         SubRing     
               
   RingHom       
     RingHom      |