Step | Hyp | Ref
| Expression |
1 | | subrgrcl 13285 |
. . . 4
 SubRing 
  |
2 | 1 | a1i 9 |
. . 3
  SubRing     |
3 | | subrgrcl 13285 |
. . . 4
 SubRing 
  |
4 | | subrgpropd.1 |
. . . . 5
       |
5 | | subrgpropd.2 |
. . . . 5
       |
6 | | subrgpropd.3 |
. . . . 5
 

                  |
7 | | subrgpropd.4 |
. . . . 5
 

                    |
8 | 4, 5, 6, 7 | ringpropd 13148 |
. . . 4
     |
9 | 3, 8 | imbitrrid 156 |
. . 3
  SubRing     |
10 | 8 | adantr 276 |
. . . . . . 7
 


   |
11 | 4 | ineq2d 3336 |
. . . . . . . . . 10
           |
12 | 11 | adantr 276 |
. . . . . . . . 9
 

          |
13 | | eqidd 2178 |
. . . . . . . . . . 11
      ↾s   ↾s    |
14 | | eqidd 2178 |
. . . . . . . . . . 11
               |
15 | | simplr 528 |
. . . . . . . . . . 11
       |
16 | | simpr 110 |
. . . . . . . . . . 11
       |
17 | 13, 14, 15, 16 | ressbasd 12519 |
. . . . . . . . . 10
     
         ↾s     |
18 | 17 | elvd 2742 |
. . . . . . . . 9
 

          ↾s     |
19 | 12, 18 | eqtrd 2210 |
. . . . . . . 8
 

      ↾s     |
20 | 5 | ineq2d 3336 |
. . . . . . . . . 10
           |
21 | 20 | adantr 276 |
. . . . . . . . 9
 

          |
22 | | eqidd 2178 |
. . . . . . . . . . 11
      ↾s   ↾s    |
23 | | eqidd 2178 |
. . . . . . . . . . 11
               |
24 | 8 | biimpa 296 |
. . . . . . . . . . . 12
 

  |
25 | 24 | adantr 276 |
. . . . . . . . . . 11
       |
26 | 22, 23, 25, 16 | ressbasd 12519 |
. . . . . . . . . 10
     
         ↾s     |
27 | 26 | elvd 2742 |
. . . . . . . . 9
 

          ↾s     |
28 | 21, 27 | eqtrd 2210 |
. . . . . . . 8
 

      ↾s     |
29 | | elinel2 3322 |
. . . . . . . . . 10
     |
30 | | elinel2 3322 |
. . . . . . . . . 10
     |
31 | 29, 30 | anim12i 338 |
. . . . . . . . 9
   
   
   |
32 | 6 | adantlr 477 |
. . . . . . . . . 10
    
 
  
             |
33 | | eqidd 2178 |
. . . . . . . . . . . . 13
             |
34 | 13, 33, 16, 15 | ressplusgd 12579 |
. . . . . . . . . . . 12
           ↾s     |
35 | 34 | elvd 2742 |
. . . . . . . . . . 11
 

      ↾s     |
36 | 35 | oveqdr 5900 |
. . . . . . . . . 10
    
 
  
         ↾s       |
37 | | eqidd 2178 |
. . . . . . . . . . . . 13
             |
38 | 22, 37, 16, 25 | ressplusgd 12579 |
. . . . . . . . . . . 12
           ↾s     |
39 | 38 | elvd 2742 |
. . . . . . . . . . 11
 

      ↾s     |
40 | 39 | oveqdr 5900 |
. . . . . . . . . 10
    
 
  
         ↾s       |
41 | 32, 36, 40 | 3eqtr3d 2218 |
. . . . . . . . 9
    
 
  
  ↾s          ↾s       |
42 | 31, 41 | sylan2 286 |
. . . . . . . 8
      
         ↾s          ↾s       |
43 | 7 | adantlr 477 |
. . . . . . . . . 10
    
 
                  |
44 | | vex 2740 |
. . . . . . . . . . . . 13
 |
45 | | eqid 2177 |
. . . . . . . . . . . . . 14
 ↾s   ↾s   |
46 | | eqid 2177 |
. . . . . . . . . . . . . 14
         |
47 | 45, 46 | ressmulrg 12595 |
. . . . . . . . . . . . 13
 
         ↾s     |
48 | 44, 47 | mpan 424 |
. . . . . . . . . . . 12

        ↾s     |
49 | 48 | adantl 277 |
. . . . . . . . . . 11
 

        ↾s     |
50 | 49 | oveqdr 5900 |
. . . . . . . . . 10
    
 
              ↾s       |
51 | | eqid 2177 |
. . . . . . . . . . . . 13
 ↾s   ↾s   |
52 | | eqid 2177 |
. . . . . . . . . . . . 13
         |
53 | 51, 52 | ressmulrg 12595 |
. . . . . . . . . . . 12
 
         ↾s     |
54 | 44, 24, 53 | sylancr 414 |
. . . . . . . . . . 11
 

        ↾s     |
55 | 54 | oveqdr 5900 |
. . . . . . . . . 10
    
 
              ↾s       |
56 | 43, 50, 55 | 3eqtr3d 2218 |
. . . . . . . . 9
    
 
      ↾s           ↾s       |
57 | 31, 56 | sylan2 286 |
. . . . . . . 8
      
          ↾s           ↾s       |
58 | 19, 28, 42, 57 | ringpropd 13148 |
. . . . . . 7
 

  ↾s   ↾s     |
59 | 10, 58 | anbi12d 473 |
. . . . . 6
 

 
 ↾s    
↾s      |
60 | 4, 5 | eqtr3d 2212 |
. . . . . . . . 9
           |
61 | 60 | sseq2d 3185 |
. . . . . . . 8
     
       |
62 | 61 | adantr 276 |
. . . . . . 7
 

            |
63 | 4 | adantr 276 |
. . . . . . . . 9
 

      |
64 | 5 | adantr 276 |
. . . . . . . . 9
 

      |
65 | | simpr 110 |
. . . . . . . . 9
 

  |
66 | 63, 64, 43, 65, 24 | rngidpropdg 13246 |
. . . . . . . 8
 

          |
67 | 66 | eleq1d 2246 |
. . . . . . 7
 

            |
68 | 62, 67 | anbi12d 473 |
. . . . . 6
 

 
        
    
        |
69 | 59, 68 | anbi12d 473 |
. . . . 5
 

   
↾s   
         
 
 ↾s                 |
70 | | eqid 2177 |
. . . . . 6
         |
71 | | eqid 2177 |
. . . . . 6
         |
72 | 70, 71 | issubrg 13280 |
. . . . 5
 SubRing   
 ↾s                |
73 | | eqid 2177 |
. . . . . 6
         |
74 | | eqid 2177 |
. . . . . 6
         |
75 | 73, 74 | issubrg 13280 |
. . . . 5
 SubRing   
 ↾s                |
76 | 69, 72, 75 | 3bitr4g 223 |
. . . 4
 

 SubRing  SubRing     |
77 | 76 | ex 115 |
. . 3
   SubRing 
SubRing      |
78 | 2, 9, 77 | pm5.21ndd 705 |
. 2
  SubRing 
SubRing     |
79 | 78 | eqrdv 2175 |
1
 SubRing  SubRing    |