Step | Hyp | Ref
| Expression |
1 | | unitpropdg.1 |
. . . . . . 7
       |
2 | | unitpropdg.2 |
. . . . . . 7
       |
3 | | unitpropdg.3 |
. . . . . . 7
 

                    |
4 | | unitpropdg.k |
. . . . . . 7
   |
5 | | unitpropdg.l |
. . . . . . 7
   |
6 | 1, 2, 3, 4, 5 | rngidpropdg 13315 |
. . . . . 6
           |
7 | 6 | breq2d 4016 |
. . . . 5
    r      
  r          |
8 | 6 | breq2d 4016 |
. . . . 5
    r oppr       
  r oppr           |
9 | 7, 8 | anbi12d 473 |
. . . 4
     r         r oppr        
   r         r oppr            |
10 | | ringsrg 13224 |
. . . . . . . 8

SRing |
11 | 4, 10 | syl 14 |
. . . . . . 7
 SRing |
12 | | ringsrg 13224 |
. . . . . . . 8

SRing |
13 | 5, 12 | syl 14 |
. . . . . . 7
 SRing |
14 | 1, 2, 3, 11, 13 | dvdsrpropdg 13316 |
. . . . . 6
  r   r    |
15 | 14 | breqd 4015 |
. . . . 5
    r      
  r          |
16 | | eqid 2177 |
. . . . . . . . . 10
oppr  oppr   |
17 | | eqid 2177 |
. . . . . . . . . 10
         |
18 | 16, 17 | opprbasg 13247 |
. . . . . . . . 9

       oppr     |
19 | 4, 18 | syl 14 |
. . . . . . . 8
        oppr     |
20 | 1, 19 | eqtrd 2210 |
. . . . . . 7
    oppr     |
21 | | eqid 2177 |
. . . . . . . . . 10
oppr  oppr   |
22 | | eqid 2177 |
. . . . . . . . . 10
         |
23 | 21, 22 | opprbasg 13247 |
. . . . . . . . 9

       oppr     |
24 | 5, 23 | syl 14 |
. . . . . . . 8
        oppr     |
25 | 2, 24 | eqtrd 2210 |
. . . . . . 7
    oppr     |
26 | 3 | ancom2s 566 |
. . . . . . . 8
 

                    |
27 | 4 | adantr 276 |
. . . . . . . . 9
 

 
  |
28 | | simprl 529 |
. . . . . . . . 9
 

    |
29 | | simprr 531 |
. . . . . . . . 9
 

 
  |
30 | | eqid 2177 |
. . . . . . . . . 10
         |
31 | | eqid 2177 |
. . . . . . . . . 10
   oppr      oppr    |
32 | 17, 30, 16, 31 | opprmulg 13243 |
. . . . . . . . 9
 
      oppr               |
33 | 27, 28, 29, 32 | syl3anc 1238 |
. . . . . . . 8
 

       oppr               |
34 | 5 | adantr 276 |
. . . . . . . . 9
 

 
  |
35 | | eqid 2177 |
. . . . . . . . . 10
         |
36 | | eqid 2177 |
. . . . . . . . . 10
   oppr      oppr    |
37 | 22, 35, 21, 36 | opprmulg 13243 |
. . . . . . . . 9
 
      oppr               |
38 | 34, 28, 29, 37 | syl3anc 1238 |
. . . . . . . 8
 

       oppr               |
39 | 26, 33, 38 | 3eqtr4d 2220 |
. . . . . . 7
 

       oppr          oppr       |
40 | 16 | opprring 13249 |
. . . . . . . 8

oppr    |
41 | | ringsrg 13224 |
. . . . . . . 8
 oppr  oppr  SRing |
42 | 4, 40, 41 | 3syl 17 |
. . . . . . 7
 oppr  SRing |
43 | 21 | opprring 13249 |
. . . . . . . 8

oppr    |
44 | | ringsrg 13224 |
. . . . . . . 8
 oppr  oppr  SRing |
45 | 5, 43, 44 | 3syl 17 |
. . . . . . 7
 oppr  SRing |
46 | 20, 25, 39, 42, 45 | dvdsrpropdg 13316 |
. . . . . 6
  r oppr    r oppr     |
47 | 46 | breqd 4015 |
. . . . 5
    r oppr       
  r oppr           |
48 | 15, 47 | anbi12d 473 |
. . . 4
     r         r oppr        
   r         r oppr            |
49 | 9, 48 | bitrd 188 |
. . 3
     r         r oppr        
   r         r oppr            |
50 | | eqidd 2178 |
. . . 4
 Unit  Unit    |
51 | | eqidd 2178 |
. . . 4
           |
52 | | eqidd 2178 |
. . . 4
  r   r    |
53 | | eqidd 2178 |
. . . 4
 oppr  oppr    |
54 | | eqidd 2178 |
. . . 4
  r oppr    r oppr     |
55 | 50, 51, 52, 53, 54, 11 | isunitd 13275 |
. . 3
  Unit 
   r         r oppr            |
56 | | eqidd 2178 |
. . . 4
 Unit  Unit    |
57 | | eqidd 2178 |
. . . 4
           |
58 | | eqidd 2178 |
. . . 4
  r   r    |
59 | | eqidd 2178 |
. . . 4
 oppr  oppr    |
60 | | eqidd 2178 |
. . . 4
  r oppr    r oppr     |
61 | 56, 57, 58, 59, 60, 13 | isunitd 13275 |
. . 3
  Unit 
   r         r oppr            |
62 | 49, 55, 61 | 3bitr4d 220 |
. 2
  Unit 
Unit     |
63 | 62 | eqrdv 2175 |
1
 Unit  Unit    |