Step | Hyp | Ref
| Expression |
1 | | subrgrcl 13285 |
. . . . 5
 SubRing 
  |
2 | 1 | adantr 276 |
. . . 4
  SubRing 
SubRing     |
3 | | eqid 2177 |
. . . . . . . . 9
         |
4 | 3 | subrgss 13281 |
. . . . . . . 8
 SubRing 
      |
5 | 4 | adantl 277 |
. . . . . . 7
  SubRing 
SubRing         |
6 | | subsubrg.s |
. . . . . . . . 9

↾s   |
7 | 6 | subrgbas 13289 |
. . . . . . . 8
 SubRing 
      |
8 | 7 | adantr 276 |
. . . . . . 7
  SubRing 
SubRing         |
9 | 5, 8 | sseqtrrd 3194 |
. . . . . 6
  SubRing 
SubRing     |
10 | 6 | oveq1i 5882 |
. . . . . . 7
 ↾s    ↾s 
↾s   |
11 | | ressabsg 12527 |
. . . . . . . . 9
  SubRing 
   ↾s  ↾s   ↾s    |
12 | 11 | 3expa 1203 |
. . . . . . . 8
   SubRing     
↾s 
↾s   ↾s    |
13 | 1, 12 | mpidan 423 |
. . . . . . 7
  SubRing 

  ↾s 
↾s   ↾s    |
14 | 10, 13 | eqtrid 2222 |
. . . . . 6
  SubRing 

 ↾s   ↾s    |
15 | 9, 14 | syldan 282 |
. . . . 5
  SubRing 
SubRing    ↾s   ↾s    |
16 | | eqid 2177 |
. . . . . . 7
 ↾s   ↾s   |
17 | 16 | subrgring 13283 |
. . . . . 6
 SubRing 
 ↾s    |
18 | 17 | adantl 277 |
. . . . 5
  SubRing 
SubRing    ↾s    |
19 | 15, 18 | eqeltrrd 2255 |
. . . 4
  SubRing 
SubRing    ↾s    |
20 | | eqid 2177 |
. . . . . . . 8
         |
21 | 20 | subrgss 13281 |
. . . . . . 7
 SubRing 
      |
22 | 21 | adantr 276 |
. . . . . 6
  SubRing 
SubRing         |
23 | 9, 22 | sstrd 3165 |
. . . . 5
  SubRing 
SubRing         |
24 | | eqid 2177 |
. . . . . . . 8
         |
25 | 6, 24 | subrg1 13290 |
. . . . . . 7
 SubRing 
          |
26 | 25 | adantr 276 |
. . . . . 6
  SubRing 
SubRing             |
27 | | eqid 2177 |
. . . . . . . 8
         |
28 | 27 | subrg1cl 13288 |
. . . . . . 7
 SubRing 
      |
29 | 28 | adantl 277 |
. . . . . 6
  SubRing 
SubRing         |
30 | 26, 29 | eqeltrd 2254 |
. . . . 5
  SubRing 
SubRing         |
31 | 23, 30 | jca 306 |
. . . 4
  SubRing 
SubRing               |
32 | 20, 24 | issubrg 13280 |
. . . 4
 SubRing   
 ↾s                |
33 | 2, 19, 31, 32 | syl21anbrc 1182 |
. . 3
  SubRing 
SubRing   SubRing    |
34 | 33, 9 | jca 306 |
. 2
  SubRing 
SubRing    SubRing 
   |
35 | 6 | subrgring 13283 |
. . . 4
 SubRing 
  |
36 | 35 | adantr 276 |
. . 3
  SubRing 
 SubRing 
 
  |
37 | 14 | adantrl 478 |
. . . 4
  SubRing 
 SubRing 
 
 ↾s   ↾s    |
38 | | eqid 2177 |
. . . . . 6
 ↾s   ↾s   |
39 | 38 | subrgring 13283 |
. . . . 5
 SubRing 
 ↾s    |
40 | 39 | ad2antrl 490 |
. . . 4
  SubRing 
 SubRing 
 
 ↾s    |
41 | 37, 40 | eqeltrd 2254 |
. . 3
  SubRing 
 SubRing 
 
 ↾s    |
42 | | simprr 531 |
. . . . 5
  SubRing 
 SubRing 
 
  |
43 | 7 | adantr 276 |
. . . . 5
  SubRing 
 SubRing 
 
      |
44 | 42, 43 | sseqtrd 3193 |
. . . 4
  SubRing 
 SubRing 
 
      |
45 | 25 | adantr 276 |
. . . . 5
  SubRing 
 SubRing 
 
          |
46 | 24 | subrg1cl 13288 |
. . . . . 6
 SubRing 
      |
47 | 46 | ad2antrl 490 |
. . . . 5
  SubRing 
 SubRing 
 
      |
48 | 45, 47 | eqeltrrd 2255 |
. . . 4
  SubRing 
 SubRing 
 
      |
49 | 44, 48 | jca 306 |
. . 3
  SubRing 
 SubRing 
 
    
       |
50 | 3, 27 | issubrg 13280 |
. . 3
 SubRing   
 ↾s                |
51 | 36, 41, 49, 50 | syl21anbrc 1182 |
. 2
  SubRing 
 SubRing 
 
SubRing    |
52 | 34, 51 | impbida 596 |
1
 SubRing 
 SubRing   SubRing 
    |