Step | Hyp | Ref
| Expression |
1 | | subrguss.3 |
. . . . . . . . 9
Unit   |
2 | 1 | a1i 9 |
. . . . . . . 8
 SubRing 
Unit    |
3 | | eqidd 2178 |
. . . . . . . 8
 SubRing 
          |
4 | | eqidd 2178 |
. . . . . . . 8
 SubRing 
 r   r    |
5 | | eqidd 2178 |
. . . . . . . 8
 SubRing 
oppr  oppr    |
6 | | eqidd 2178 |
. . . . . . . 8
 SubRing 
 r oppr    r oppr     |
7 | | subrguss.1 |
. . . . . . . . . 10

↾s   |
8 | 7 | subrgring 13283 |
. . . . . . . . 9
 SubRing 
  |
9 | | ringsrg 13155 |
. . . . . . . . 9

SRing |
10 | 8, 9 | syl 14 |
. . . . . . . 8
 SubRing 
SRing |
11 | 2, 3, 4, 5, 6, 10 | isunitd 13206 |
. . . . . . 7
 SubRing 

   r         r oppr            |
12 | 11 | simprbda 383 |
. . . . . 6
  SubRing 
   r         |
13 | | eqid 2177 |
. . . . . . . 8
         |
14 | 7, 13 | subrg1 13290 |
. . . . . . 7
 SubRing 
          |
15 | 14 | adantr 276 |
. . . . . 6
  SubRing 
           |
16 | 12, 15 | breqtrrd 4030 |
. . . . 5
  SubRing 
   r         |
17 | | eqid 2177 |
. . . . . . . 8
 r   r   |
18 | | eqid 2177 |
. . . . . . . 8
 r   r   |
19 | 7, 17, 18 | subrgdvds 13294 |
. . . . . . 7
 SubRing 
 r 
 r    |
20 | 19 | adantr 276 |
. . . . . 6
  SubRing 
  r   r    |
21 | 20 | ssbrd 4045 |
. . . . 5
  SubRing 
    r         r          |
22 | 16, 21 | mpd 13 |
. . . 4
  SubRing 
   r         |
23 | | subrgrcl 13285 |
. . . . . . . 8
 SubRing 
  |
24 | 23 | adantr 276 |
. . . . . . 7
  SubRing 
   |
25 | | eqid 2177 |
. . . . . . . 8
oppr  oppr   |
26 | | eqid 2177 |
. . . . . . . 8
         |
27 | 25, 26 | opprbasg 13178 |
. . . . . . 7

       oppr     |
28 | 24, 27 | syl 14 |
. . . . . 6
  SubRing 
        oppr     |
29 | | eqidd 2178 |
. . . . . 6
  SubRing 
  r oppr    r oppr     |
30 | 25 | opprring 13180 |
. . . . . . 7

oppr    |
31 | | ringsrg 13155 |
. . . . . . 7
 oppr  oppr  SRing |
32 | 24, 30, 31 | 3syl 17 |
. . . . . 6
  SubRing 
 oppr 
SRing |
33 | | eqidd 2178 |
. . . . . 6
  SubRing 
    oppr      oppr     |
34 | 7 | subrgbas 13289 |
. . . . . . . . 9
 SubRing 
      |
35 | 34 | adantr 276 |
. . . . . . . 8
  SubRing 
       |
36 | 26 | subrgss 13281 |
. . . . . . . . 9
 SubRing 
      |
37 | 36 | adantr 276 |
. . . . . . . 8
  SubRing 
       |
38 | 35, 37 | eqsstrrd 3192 |
. . . . . . 7
  SubRing 
           |
39 | | eqidd 2178 |
. . . . . . . 8
  SubRing 
           |
40 | 1 | a1i 9 |
. . . . . . . 8
  SubRing 
 Unit    |
41 | 10 | adantr 276 |
. . . . . . . 8
  SubRing 
 SRing |
42 | | simpr 110 |
. . . . . . . 8
  SubRing 
   |
43 | 39, 40, 41, 42 | unitcld 13208 |
. . . . . . 7
  SubRing 
       |
44 | 38, 43 | sseldd 3156 |
. . . . . 6
  SubRing 
       |
45 | | eqid 2177 |
. . . . . . . . 9
         |
46 | | eqid 2177 |
. . . . . . . . 9
         |
47 | 1, 45, 46 | ringinvcl 13225 |
. . . . . . . 8
                 |
48 | 8, 47 | sylan 283 |
. . . . . . 7
  SubRing 
               |
49 | 38, 48 | sseldd 3156 |
. . . . . 6
  SubRing 
               |
50 | 28, 29, 32, 33, 44, 49 | dvdsrmuld 13196 |
. . . . 5
  SubRing 
   r oppr                 oppr       |
51 | 1, 45 | unitinvcl 13223 |
. . . . . . . 8
             |
52 | 8, 51 | sylan 283 |
. . . . . . 7
  SubRing 
           |
53 | | eqid 2177 |
. . . . . . . 8
         |
54 | | eqid 2177 |
. . . . . . . 8
   oppr      oppr    |
55 | 26, 53, 25, 54 | opprmulg 13174 |
. . . . . . 7
         

             oppr                       |
56 | 24, 52, 42, 55 | syl3anc 1238 |
. . . . . 6
  SubRing 
              oppr                       |
57 | | eqid 2177 |
. . . . . . . . 9
         |
58 | | eqid 2177 |
. . . . . . . . 9
         |
59 | 1, 45, 57, 58 | unitrinv 13227 |
. . . . . . . 8
                         |
60 | 8, 59 | sylan 283 |
. . . . . . 7
  SubRing 
                       |
61 | 7, 53 | ressmulrg 12595 |
. . . . . . . . . 10
  SubRing 

          |
62 | 23, 61 | mpdan 421 |
. . . . . . . . 9
 SubRing 
          |
63 | 62 | adantr 276 |
. . . . . . . 8
  SubRing 
           |
64 | 63 | oveqd 5889 |
. . . . . . 7
  SubRing 
                                   |
65 | 60, 64, 15 | 3eqtr4d 2220 |
. . . . . 6
  SubRing 
                       |
66 | 56, 65 | eqtrd 2210 |
. . . . 5
  SubRing 
              oppr           |
67 | 50, 66 | breqtrd 4028 |
. . . 4
  SubRing 
   r oppr          |
68 | | subrguss.2 |
. . . . . . 7
Unit   |
69 | 68 | a1i 9 |
. . . . . 6
 SubRing 
Unit    |
70 | | eqidd 2178 |
. . . . . 6
 SubRing 
          |
71 | | eqidd 2178 |
. . . . . 6
 SubRing 
 r   r    |
72 | | eqidd 2178 |
. . . . . 6
 SubRing 
oppr  oppr    |
73 | | eqidd 2178 |
. . . . . 6
 SubRing 
 r oppr    r oppr     |
74 | | ringsrg 13155 |
. . . . . . 7

SRing |
75 | 23, 74 | syl 14 |
. . . . . 6
 SubRing 
SRing |
76 | 69, 70, 71, 72, 73, 75 | isunitd 13206 |
. . . . 5
 SubRing 

   r         r oppr            |
77 | 76 | adantr 276 |
. . . 4
  SubRing 
 
   r         r oppr            |
78 | 22, 67, 77 | mpbir2and 944 |
. . 3
  SubRing 
   |
79 | 78 | ex 115 |
. 2
 SubRing 

   |
80 | 79 | ssrdv 3161 |
1
 SubRing 
  |