Step | Hyp | Ref
| Expression |
1 | | isdrng2.b |
. . 3
     |
2 | | eqid 2451 |
. . 3
Unit  Unit   |
3 | | isdrng2.z |
. . 3
     |
4 | 1, 2, 3 | isdrng 17979 |
. 2
  Unit       |
5 | | oveq2 6298 |
. . . . . . 7
 Unit   
 mulGrp 
↾s Unit    mulGrp 
↾s      |
6 | 5 | adantl 468 |
. . . . . 6
  Unit      mulGrp  ↾s Unit    mulGrp  ↾s      |
7 | | isdrng2.g |
. . . . . 6
 mulGrp  ↾s     |
8 | 6, 7 | syl6eqr 2503 |
. . . . 5
  Unit      mulGrp  ↾s Unit     |
9 | | eqid 2451 |
. . . . . . 7
 mulGrp 
↾s Unit    mulGrp 
↾s Unit    |
10 | 2, 9 | unitgrp 17895 |
. . . . . 6

 mulGrp 
↾s Unit     |
11 | 10 | adantr 467 |
. . . . 5
  Unit      mulGrp  ↾s Unit     |
12 | 8, 11 | eqeltrrd 2530 |
. . . 4
  Unit       |
13 | 1, 2 | unitcl 17887 |
. . . . . . . . 9
 Unit 
  |
14 | 13 | adantl 468 |
. . . . . . . 8
   
Unit  
  |
15 | | difss 3560 |
. . . . . . . . . . . . . . 15
 
 |
16 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
mulGrp  mulGrp   |
17 | 16, 1 | mgpbas 17729 |
. . . . . . . . . . . . . . . 16
   mulGrp    |
18 | 7, 17 | ressbas2 15180 |
. . . . . . . . . . . . . . 15
  
        |
19 | 15, 18 | ax-mp 5 |
. . . . . . . . . . . . . 14
       |
20 | | eqid 2451 |
. . . . . . . . . . . . . 14
         |
21 | 19, 20 | grpidcl 16694 |
. . . . . . . . . . . . 13
         |
22 | 21 | ad2antlr 733 |
. . . . . . . . . . . 12
   
Unit           |
23 | | eldifsn 4097 |
. . . . . . . . . . . 12
      
           |
24 | 22, 23 | sylib 200 |
. . . . . . . . . . 11
   
Unit              |
25 | 24 | simprd 465 |
. . . . . . . . . 10
   
Unit        |
26 | | simpll 760 |
. . . . . . . . . . 11
   
Unit  
  |
27 | 22 | eldifad 3416 |
. . . . . . . . . . 11
   
Unit         |
28 | | simpr 463 |
. . . . . . . . . . 11
   
Unit  
Unit    |
29 | | eqid 2451 |
. . . . . . . . . . . 12
/r  /r   |
30 | | eqid 2451 |
. . . . . . . . . . . 12
         |
31 | 1, 2, 29, 30 | dvrcan1 17919 |
. . . . . . . . . . 11
      Unit  
       /r                 |
32 | 26, 27, 28, 31 | syl3anc 1268 |
. . . . . . . . . 10
   
Unit          /r                 |
33 | 1, 2, 29 | dvrcl 17914 |
. . . . . . . . . . . 12
      Unit  
      /r      |
34 | 26, 27, 28, 33 | syl3anc 1268 |
. . . . . . . . . . 11
   
Unit         /r      |
35 | 1, 30, 3 | ringrz 17818 |
. . . . . . . . . . 11
        /r            /r          |
36 | 26, 34, 35 | syl2anc 667 |
. . . . . . . . . 10
   
Unit          /r          |
37 | 25, 32, 36 | 3netr4d 2701 |
. . . . . . . . 9
   
Unit          /r                  /r           |
38 | | oveq2 6298 |
. . . . . . . . . 10
        /r                  /r           |
39 | 38 | necon3i 2656 |
. . . . . . . . 9
        /r                  /r          |
40 | 37, 39 | syl 17 |
. . . . . . . 8
   
Unit    |
41 | | eldifsn 4097 |
. . . . . . . 8
  

  |
42 | 14, 40, 41 | sylanbrc 670 |
. . . . . . 7
   
Unit  
    |
43 | 42 | ex 436 |
. . . . . 6
    Unit       |
44 | 43 | ssrdv 3438 |
. . . . 5
   Unit      |
45 | | eldifi 3555 |
. . . . . . . . . . 11
  
  |
46 | 45 | adantl 468 |
. . . . . . . . . 10
   
     |
47 | | eqid 2451 |
. . . . . . . . . . . . 13
           |
48 | 19, 47 | grpinvcl 16711 |
. . . . . . . . . . . 12
 
  
             |
49 | 48 | adantll 720 |
. . . . . . . . . . 11
   
                |
50 | 49 | eldifad 3416 |
. . . . . . . . . 10
   
              |
51 | | eqid 2451 |
. . . . . . . . . . 11
 r   r   |
52 | 1, 51, 30 | dvdsrmul 17876 |
. . . . . . . . . 10
              r                      |
53 | 46, 50, 52 | syl2anc 667 |
. . . . . . . . 9
   
     r                      |
54 | | fvex 5875 |
. . . . . . . . . . . . . 14
     |
55 | 1, 54 | eqeltri 2525 |
. . . . . . . . . . . . 13
 |
56 | | difexg 4551 |
. . . . . . . . . . . . 13
     |
57 | 16, 30 | mgpplusg 17727 |
. . . . . . . . . . . . . 14
      mulGrp    |
58 | 7, 57 | ressplusg 15239 |
. . . . . . . . . . . . 13
            |
59 | 55, 56, 58 | mp2b 10 |
. . . . . . . . . . . 12
        |
60 | 19, 59, 20, 47 | grplinv 16712 |
. . . . . . . . . . 11
 
  
                       |
61 | 60 | adantll 720 |
. . . . . . . . . 10
   
                          |
62 | | eqid 2451 |
. . . . . . . . . . . . . . 15
         |
63 | 1, 62 | ringidcl 17801 |
. . . . . . . . . . . . . 14

      |
64 | 1, 30, 62 | ringlidm 17804 |
. . . . . . . . . . . . . 14
                             |
65 | 63, 64 | mpdan 674 |
. . . . . . . . . . . . 13

                      |
66 | 65 | adantr 467 |
. . . . . . . . . . . 12
                         |
67 | | simpr 463 |
. . . . . . . . . . . . 13
     |
68 | 2, 62 | 1unit 17886 |
. . . . . . . . . . . . . . 15

    Unit    |
69 | 68 | adantr 467 |
. . . . . . . . . . . . . 14
       Unit    |
70 | 44, 69 | sseldd 3433 |
. . . . . . . . . . . . 13
           |
71 | 19, 59, 20 | grpid 16701 |
. . . . . . . . . . . . 13
                                         |
72 | 67, 70, 71 | syl2anc 667 |
. . . . . . . . . . . 12
                       
           |
73 | 66, 72 | mpbid 214 |
. . . . . . . . . . 11
             |
74 | 73 | adantr 467 |
. . . . . . . . . 10
   
             |
75 | 61, 74 | eqtrd 2485 |
. . . . . . . . 9
   
                          |
76 | 53, 75 | breqtrd 4427 |
. . . . . . . 8
   
     r         |
77 | | eqid 2451 |
. . . . . . . . . . . 12
oppr  oppr   |
78 | 77, 1 | opprbas 17857 |
. . . . . . . . . . 11
   oppr    |
79 | | eqid 2451 |
. . . . . . . . . . 11
 r oppr    r oppr    |
80 | | eqid 2451 |
. . . . . . . . . . 11
   oppr      oppr    |
81 | 78, 79, 80 | dvdsrmul 17876 |
. . . . . . . . . 10
              r oppr                  oppr       |
82 | 46, 50, 81 | syl2anc 667 |
. . . . . . . . 9
   
     r oppr                  oppr       |
83 | 1, 30, 77, 80 | opprmul 17854 |
. . . . . . . . . 10
              oppr                       |
84 | 19, 59, 20, 47 | grprinv 16713 |
. . . . . . . . . . . 12
 
  
                       |
85 | 84 | adantll 720 |
. . . . . . . . . . 11
   
                          |
86 | 85, 74 | eqtrd 2485 |
. . . . . . . . . 10
   
                          |
87 | 83, 86 | syl5eq 2497 |
. . . . . . . . 9
   
                 oppr           |
88 | 82, 87 | breqtrd 4427 |
. . . . . . . 8
   
     r oppr          |
89 | 2, 62, 51, 77, 79 | isunit 17885 |
. . . . . . . 8
 Unit     r         r oppr           |
90 | 76, 88, 89 | sylanbrc 670 |
. . . . . . 7
   
   Unit    |
91 | 90 | ex 436 |
. . . . . 6
     
Unit     |
92 | 91 | ssrdv 3438 |
. . . . 5
    
Unit    |
93 | 44, 92 | eqssd 3449 |
. . . 4
   Unit      |
94 | 12, 93 | impbida 843 |
. . 3

 Unit   
   |
95 | 94 | pm5.32i 643 |
. 2
  Unit    

   |
96 | 4, 95 | bitri 253 |
1
     |