Step | Hyp | Ref
| Expression |
1 | | subrgugrp.1 |
. . . . 5

↾s   |
2 | | subrgugrp.2 |
. . . . 5
Unit   |
3 | | subrgugrp.3 |
. . . . 5
Unit   |
4 | 1, 2, 3 | subrguss 13295 |
. . . 4
 SubRing 
  |
5 | 4 | sselda 3155 |
. . 3
  SubRing 
   |
6 | 1 | subrgbas 13289 |
. . . . 5
 SubRing 
      |
7 | 6 | adantr 276 |
. . . 4
  SubRing 
       |
8 | 3 | a1i 9 |
. . . 4
  SubRing 
 Unit    |
9 | 1 | subrgring 13283 |
. . . . . 6
 SubRing 
  |
10 | | ringsrg 13155 |
. . . . . 6

SRing |
11 | 9, 10 | syl 14 |
. . . . 5
 SubRing 
SRing |
12 | 11 | adantr 276 |
. . . 4
  SubRing 
 SRing |
13 | | simpr 110 |
. . . 4
  SubRing 
   |
14 | 7, 8, 12, 13 | unitcld 13208 |
. . 3
  SubRing 
   |
15 | | eqid 2177 |
. . . . . 6
         |
16 | | eqid 2177 |
. . . . . 6
         |
17 | 3, 15, 16 | ringinvcl 13225 |
. . . . 5
                 |
18 | 9, 17 | sylan 283 |
. . . 4
  SubRing 
               |
19 | | subrgunit.4 |
. . . . 5
     |
20 | 1, 19, 3, 15 | subrginv 13296 |
. . . 4
  SubRing 
               |
21 | 18, 20, 7 | 3eltr4d 2261 |
. . 3
  SubRing 
       |
22 | 5, 14, 21 | 3jca 1177 |
. 2
  SubRing 
 
       |
23 | | eqidd 2178 |
. . . . 5
  SubRing 

                |
24 | | eqidd 2178 |
. . . . 5
  SubRing 

       r   r    |
25 | 11 | adantr 276 |
. . . . 5
  SubRing 

     
SRing |
26 | | eqidd 2178 |
. . . . 5
  SubRing 

                |
27 | | simpr2 1004 |
. . . . . 6
  SubRing 

     
  |
28 | 6 | adantr 276 |
. . . . . 6
  SubRing 

     
      |
29 | 27, 28 | eleqtrd 2256 |
. . . . 5
  SubRing 

     
      |
30 | | simpr3 1005 |
. . . . . 6
  SubRing 

            |
31 | 30, 28 | eleqtrd 2256 |
. . . . 5
  SubRing 

                |
32 | 23, 24, 25, 26, 29, 31 | dvdsrmuld 13196 |
. . . 4
  SubRing 

        r                 |
33 | | subrgrcl 13285 |
. . . . . 6
 SubRing 
  |
34 | | simpr1 1003 |
. . . . . 6
  SubRing 

     
  |
35 | | eqid 2177 |
. . . . . . 7
         |
36 | | eqid 2177 |
. . . . . . 7
         |
37 | 2, 19, 35, 36 | unitlinv 13226 |
. . . . . 6
                     |
38 | 33, 34, 37 | syl2an2r 595 |
. . . . 5
  SubRing 

                        |
39 | 1, 35 | ressmulrg 12595 |
. . . . . . . 8
  SubRing 

          |
40 | 33, 39 | mpdan 421 |
. . . . . . 7
 SubRing 
          |
41 | 40 | adantr 276 |
. . . . . 6
  SubRing 

                |
42 | 41 | oveqd 5889 |
. . . . 5
  SubRing 

                                |
43 | 1, 36 | subrg1 13290 |
. . . . . 6
 SubRing 
          |
44 | 43 | adantr 276 |
. . . . 5
  SubRing 

                |
45 | 38, 42, 44 | 3eqtr3d 2218 |
. . . 4
  SubRing 

                        |
46 | 32, 45 | breqtrd 4028 |
. . 3
  SubRing 

        r         |
47 | 9 | adantr 276 |
. . . . . 6
  SubRing 

     
  |
48 | | eqid 2177 |
. . . . . . 7
oppr  oppr   |
49 | 48, 16 | opprbasg 13178 |
. . . . . 6

       oppr     |
50 | 47, 49 | syl 14 |
. . . . 5
  SubRing 

             oppr     |
51 | | eqidd 2178 |
. . . . 5
  SubRing 

       r oppr    r oppr     |
52 | 48 | opprring 13180 |
. . . . . 6

oppr    |
53 | | ringsrg 13155 |
. . . . . 6
 oppr  oppr  SRing |
54 | 47, 52, 53 | 3syl 17 |
. . . . 5
  SubRing 

      oppr  SRing |
55 | | eqidd 2178 |
. . . . 5
  SubRing 

         oppr      oppr     |
56 | 50, 51, 54, 55, 29, 31 | dvdsrmuld 13196 |
. . . 4
  SubRing 

        r oppr             oppr       |
57 | | eqid 2177 |
. . . . . . 7
         |
58 | | eqid 2177 |
. . . . . . 7
   oppr      oppr    |
59 | 16, 57, 48, 58 | opprmulg 13174 |
. . . . . 6
         
    
         oppr                   |
60 | 47, 31, 29, 59 | syl3anc 1238 |
. . . . 5
  SubRing 

               oppr                   |
61 | 2, 19, 35, 36 | unitrinv 13227 |
. . . . . . 7
                     |
62 | 33, 34, 61 | syl2an2r 595 |
. . . . . 6
  SubRing 

                        |
63 | 41 | oveqd 5889 |
. . . . . 6
  SubRing 

                                |
64 | 62, 63, 44 | 3eqtr3d 2218 |
. . . . 5
  SubRing 

                        |
65 | 60, 64 | eqtrd 2210 |
. . . 4
  SubRing 

               oppr           |
66 | 56, 65 | breqtrd 4028 |
. . 3
  SubRing 

        r oppr          |
67 | 3 | a1i 9 |
. . . . 5
 SubRing 
Unit    |
68 | | eqidd 2178 |
. . . . 5
 SubRing 
          |
69 | | eqidd 2178 |
. . . . 5
 SubRing 
 r   r    |
70 | | eqidd 2178 |
. . . . 5
 SubRing 
oppr  oppr    |
71 | | eqidd 2178 |
. . . . 5
 SubRing 
 r oppr    r oppr     |
72 | 67, 68, 69, 70, 71, 11 | isunitd 13206 |
. . . 4
 SubRing 

   r         r oppr            |
73 | 72 | adantr 276 |
. . 3
  SubRing 

          r         r oppr            |
74 | 46, 66, 73 | mpbir2and 944 |
. 2
  SubRing 

     
  |
75 | 22, 74 | impbida 596 |
1
 SubRing 

         |