Step | Hyp | Ref
| Expression |
1 | | unitgrp.1 |
. . . 4
Unit   |
2 | 1 | a1i 9 |
. . 3

Unit    |
3 | | unitgrp.2 |
. . . 4
 mulGrp  ↾s   |
4 | 3 | a1i 9 |
. . 3

 mulGrp  ↾s    |
5 | | ringsrg 13177 |
. . 3

SRing |
6 | 2, 4, 5 | unitgrpbasd 13237 |
. 2

      |
7 | | eqid 2177 |
. . . 4
mulGrp  mulGrp   |
8 | | eqid 2177 |
. . . 4
         |
9 | 7, 8 | mgpplusgg 13087 |
. . 3

      mulGrp     |
10 | | basfn 12514 |
. . . . 5
 |
11 | | elex 2748 |
. . . . 5

  |
12 | | funfvex 5532 |
. . . . . 6
 
       |
13 | 12 | funfni 5316 |
. . . . 5
 
       |
14 | 10, 11, 13 | sylancr 414 |
. . . 4

      |
15 | | eqidd 2178 |
. . . . 5

          |
16 | 15, 2, 5 | unitssd 13231 |
. . . 4

      |
17 | 14, 16 | ssexd 4143 |
. . 3

  |
18 | 7 | mgpex 13088 |
. . 3

mulGrp    |
19 | 4, 9, 17, 18 | ressplusgd 12581 |
. 2

         |
20 | 1, 8 | unitmulcl 13235 |
. 2
 
           |
21 | | eqidd 2178 |
. . . . 5
  
 
          |
22 | 1 | a1i 9 |
. . . . 5
  
 
Unit    |
23 | 5 | adantr 276 |
. . . . 5
  
 
SRing |
24 | | simpr1 1003 |
. . . . 5
  
 
  |
25 | 21, 22, 23, 24 | unitcld 13230 |
. . . 4
  
 
      |
26 | | simpr2 1004 |
. . . . 5
  
 
  |
27 | 21, 22, 23, 26 | unitcld 13230 |
. . . 4
  
 
      |
28 | | simpr3 1005 |
. . . . 5
  
 
  |
29 | 21, 22, 23, 28 | unitcld 13230 |
. . . 4
  
 
      |
30 | 25, 27, 29 | 3jca 1177 |
. . 3
  
 
    
   
       |
31 | | eqid 2177 |
. . . 4
         |
32 | 31, 8 | ringass 13152 |
. . 3
          
                                        |
33 | 30, 32 | syldan 282 |
. 2
  
 
                                  |
34 | | eqid 2177 |
. . 3
         |
35 | 1, 34 | 1unit 13229 |
. 2

      |
36 | | eqidd 2178 |
. . . 4
             |
37 | 1 | a1i 9 |
. . . 4
   Unit    |
38 | 5 | adantr 276 |
. . . 4
   SRing |
39 | | simpr 110 |
. . . 4
     |
40 | 36, 37, 38, 39 | unitcld 13230 |
. . 3
         |
41 | 31, 8, 34 | ringlidm 13159 |
. . 3
                     |
42 | 40, 41 | syldan 282 |
. 2
                 |
43 | | eqidd 2178 |
. . . . 5
             |
44 | | eqidd 2178 |
. . . . 5
    r   r    |
45 | | eqidd 2178 |
. . . . 5
   oppr  oppr    |
46 | | eqidd 2178 |
. . . . 5
    r oppr    r oppr     |
47 | 37, 43, 44, 45, 46, 38 | isunitd 13228 |
. . . 4
   
   r         r oppr            |
48 | 39, 47 | mpbid 147 |
. . 3
      r         r oppr           |
49 | | eqidd 2178 |
. . . . . 6
             |
50 | 36, 44, 38, 49, 40 | dvdsr2d 13217 |
. . . . 5
      r       
                    |
51 | | eqid 2177 |
. . . . . . . 8
oppr  oppr   |
52 | 51, 31 | opprbasg 13200 |
. . . . . . 7

       oppr     |
53 | 52 | adantr 276 |
. . . . . 6
          oppr     |
54 | 51 | opprring 13202 |
. . . . . . . 8

oppr    |
55 | | ringsrg 13177 |
. . . . . . . 8
 oppr  oppr  SRing |
56 | 54, 55 | syl 14 |
. . . . . . 7

oppr 
SRing |
57 | 56 | adantr 276 |
. . . . . 6
   oppr 
SRing |
58 | | eqidd 2178 |
. . . . . 6
      oppr      oppr     |
59 | 53, 46, 57, 58, 40 | dvdsr2d 13217 |
. . . . 5
      r oppr                   oppr            |
60 | 50, 59 | anbi12d 473 |
. . . 4
       r         r oppr        
 
                
           oppr             |
61 | | reeanv 2646 |
. . . . 5
                         
     oppr         
 
                
           oppr            |
62 | | eqidd 2178 |
. . . . . . . . . . . 12
    
    
    
                  oppr                      |
63 | | eqidd 2178 |
. . . . . . . . . . . 12
    
    
    
                  oppr             r   r    |
64 | 38 | ad2antrr 488 |
. . . . . . . . . . . 12
    
    
    
                  oppr            SRing |
65 | | eqidd 2178 |
. . . . . . . . . . . 12
    
    
    
                  oppr                      |
66 | | simprl 529 |
. . . . . . . . . . . 12
    
    
    
                  oppr                  |
67 | 40 | ad2antrr 488 |
. . . . . . . . . . . 12
    
    
    
                  oppr                  |
68 | 62, 63, 64, 65, 66, 67 | dvdsrmuld 13218 |
. . . . . . . . . . 11
    
    
    
                  oppr              r             |
69 | | simplll 533 |
. . . . . . . . . . . . . 14
    
    
    
                  oppr              |
70 | | simplr 528 |
. . . . . . . . . . . . . 14
    
    
    
                  oppr                  |
71 | 31, 8 | ringass 13152 |
. . . . . . . . . . . . . 14
          
                                        |
72 | 69, 70, 67, 66, 71 | syl13anc 1240 |
. . . . . . . . . . . . 13
    
    
    
                  oppr                                              |
73 | | simprrl 539 |
. . . . . . . . . . . . . 14
    
    
    
                  oppr                          |
74 | 73 | oveq1d 5889 |
. . . . . . . . . . . . 13
    
    
    
                  oppr                                          |
75 | 39 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
    
    
    
                  oppr              |
76 | | eqid 2177 |
. . . . . . . . . . . . . . . . 17
   oppr      oppr    |
77 | 31, 8, 51, 76 | opprmulg 13196 |
. . . . . . . . . . . . . . . 16
     
      oppr               |
78 | 69, 66, 75, 77 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
    
    
    
                  oppr                 oppr               |
79 | | simprrr 540 |
. . . . . . . . . . . . . . 15
    
    
    
                  oppr                 oppr           |
80 | 78, 79 | eqtr3d 2212 |
. . . . . . . . . . . . . 14
    
    
    
                  oppr                          |
81 | 80 | oveq2d 5890 |
. . . . . . . . . . . . 13
    
    
    
                  oppr                                          |
82 | 72, 74, 81 | 3eqtr3d 2218 |
. . . . . . . . . . . 12
    
    
    
                  oppr                                      |
83 | 31, 8, 34 | ringlidm 13159 |
. . . . . . . . . . . . 13
                     |
84 | 69, 66, 83 | syl2anc 411 |
. . . . . . . . . . . 12
    
    
    
                  oppr                          |
85 | 31, 8, 34 | ringridm 13160 |
. . . . . . . . . . . . 13
                     |
86 | 69, 70, 85 | syl2anc 411 |
. . . . . . . . . . . 12
    
    
    
                  oppr                          |
87 | 82, 84, 86 | 3eqtr3d 2218 |
. . . . . . . . . . 11
    
    
    
                  oppr              |
88 | 68, 87, 80 | 3brtr3d 4034 |
. . . . . . . . . 10
    
    
    
                  oppr              r         |
89 | 69, 52 | syl 14 |
. . . . . . . . . . . 12
    
    
    
                  oppr                   oppr     |
90 | | eqidd 2178 |
. . . . . . . . . . . 12
    
    
    
                  oppr             r oppr    r oppr     |
91 | 69, 56 | syl 14 |
. . . . . . . . . . . 12
    
    
    
                  oppr            oppr 
SRing |
92 | | eqidd 2178 |
. . . . . . . . . . . 12
    
    
    
                  oppr               oppr      oppr     |
93 | 89, 90, 91, 92, 70, 67 | dvdsrmuld 13218 |
. . . . . . . . . . 11
    
    
    
                  oppr              r oppr         oppr       |
94 | 31, 8, 51, 76 | opprmulg 13196 |
. . . . . . . . . . . . 13
 
          oppr               |
95 | 69, 75, 70, 94 | syl3anc 1238 |
. . . . . . . . . . . 12
    
    
    
                  oppr                 oppr               |
96 | 95, 73 | eqtrd 2210 |
. . . . . . . . . . 11
    
    
    
                  oppr                 oppr           |
97 | 93, 96 | breqtrd 4029 |
. . . . . . . . . 10
    
    
    
                  oppr              r oppr          |
98 | 1 | a1i 9 |
. . . . . . . . . . 11
    
    
    
                  oppr            Unit    |
99 | | eqidd 2178 |
. . . . . . . . . . 11
    
    
    
                  oppr                      |
100 | | eqidd 2178 |
. . . . . . . . . . 11
    
    
    
                  oppr            oppr  oppr    |
101 | 98, 99, 63, 100, 90, 64 | isunitd 13228 |
. . . . . . . . . 10
    
    
    
                  oppr            
   r         r oppr            |
102 | 88, 97, 101 | mpbir2and 944 |
. . . . . . . . 9
    
    
    
                  oppr              |
103 | 102, 73 | jca 306 |
. . . . . . . 8
    
    
    
                  oppr                            |
104 | 103 | rexlimdvaa 2595 |
. . . . . . 7
        
 
                       oppr                           |
105 | 104 | expimpd 363 |
. . . . . 6
                                 oppr                            |
106 | 105 | reximdv2 2576 |
. . . . 5
    
                             oppr                          |
107 | 61, 106 | biimtrrid 153 |
. . . 4
                                  oppr          
               |
108 | 60, 107 | sylbid 150 |
. . 3
       r         r oppr         
               |
109 | 48, 108 | mpd 13 |
. 2
   
              |
110 | 6, 19, 20, 33, 35, 42, 109 | isgrpde 12852 |
1

  |