Proof of Theorem rdivmuldivd
Step | Hyp | Ref
| Expression |
1 | | dvrdir.b |
. . . . . 6
     |
2 | 1 | a1i 9 |
. . . . 5
       |
3 | | rdivmuldivd.p |
. . . . . 6
     |
4 | 3 | a1i 9 |
. . . . 5
       |
5 | | dvrdir.u |
. . . . . 6
Unit   |
6 | 5 | a1i 9 |
. . . . 5
 Unit    |
7 | | eqidd 2178 |
. . . . 5
           |
8 | | dvrdir.t |
. . . . . 6
/r   |
9 | 8 | a1i 9 |
. . . . 5
 /r    |
10 | | rdivmuldivd.r |
. . . . . 6
   |
11 | 10 | crngringd 13197 |
. . . . 5
   |
12 | | rdivmuldivd.a |
. . . . 5
   |
13 | | rdivmuldivd.b |
. . . . 5
   |
14 | 2, 4, 6, 7, 9, 11,
12, 13 | dvrvald 13308 |
. . . 4
               |
15 | 14 | oveq1d 5892 |
. . 3
                       |
16 | | ringsrg 13229 |
. . . . . . 7

SRing |
17 | 11, 16 | syl 14 |
. . . . . 6
 SRing |
18 | 2, 6, 17 | unitssd 13283 |
. . . . 5

  |
19 | | eqid 2177 |
. . . . . . 7
         |
20 | 5, 19 | unitinvcl 13297 |
. . . . . 6
             |
21 | 11, 13, 20 | syl2anc 411 |
. . . . 5
           |
22 | 18, 21 | sseldd 3158 |
. . . 4
           |
23 | | rdivmuldivd.c |
. . . . 5
   |
24 | | rdivmuldivd.d |
. . . . 5
   |
25 | 1, 5, 8 | dvrcl 13309 |
. . . . 5
 
     |
26 | 11, 23, 24, 25 | syl3anc 1238 |
. . . 4
     |
27 | 1, 3 | ringass 13204 |
. . . 4
  
       
              
                   |
28 | 11, 12, 22, 26, 27 | syl13anc 1240 |
. . 3
           
                   |
29 | 1, 3 | crngcom 13202 |
. . . . 5
                                       |
30 | 10, 22, 26, 29 | syl3anc 1238 |
. . . 4
         
                 |
31 | 30 | oveq2d 5893 |
. . 3
                  
            |
32 | 15, 28, 31 | 3eqtrd 2214 |
. 2
                       |
33 | | eqid 2177 |
. . . . . . . . 9
 mulGrp 
↾s   mulGrp  ↾s   |
34 | 5, 33 | unitgrp 13290 |
. . . . . . . 8

 mulGrp 
↾s    |
35 | 11, 34 | syl 14 |
. . . . . . 7
  mulGrp  ↾s    |
36 | | eqidd 2178 |
. . . . . . . . 9
  mulGrp  ↾s   mulGrp  ↾s    |
37 | 6, 36, 17 | unitgrpbasd 13289 |
. . . . . . . 8
     mulGrp  ↾s     |
38 | 13, 37 | eleqtrd 2256 |
. . . . . . 7
     mulGrp  ↾s     |
39 | 24, 37 | eleqtrd 2256 |
. . . . . . 7
     mulGrp  ↾s     |
40 | | eqid 2177 |
. . . . . . . 8
    mulGrp  ↾s       mulGrp  ↾s    |
41 | | eqid 2177 |
. . . . . . . 8
   mulGrp  ↾s      mulGrp  ↾s    |
42 | | eqid 2177 |
. . . . . . . 8
     mulGrp 
↾s        mulGrp  ↾s    |
43 | 40, 41, 42 | grpinvadd 12953 |
. . . . . . 7
   mulGrp  ↾s      mulGrp  ↾s  
    mulGrp  ↾s          mulGrp 
↾s          mulGrp  ↾s             mulGrp  ↾s          mulGrp  ↾s          mulGrp  ↾s         |
44 | 35, 38, 39, 43 | syl3anc 1238 |
. . . . . 6
       mulGrp  ↾s          mulGrp  ↾s             mulGrp  ↾s          mulGrp  ↾s          mulGrp  ↾s         |
45 | 6, 36, 7, 11 | invrfvald 13296 |
. . . . . . 7
          mulGrp 
↾s     |
46 | 45 | fveq1d 5519 |
. . . . . 6
          
  mulGrp 
↾s            mulGrp  ↾s          mulGrp  ↾s        |
47 | 45 | fveq1d 5519 |
. . . . . . 7
               mulGrp 
↾s        |
48 | 45 | fveq1d 5519 |
. . . . . . 7
               mulGrp 
↾s        |
49 | 47, 48 | oveq12d 5895 |
. . . . . 6
              mulGrp  ↾s                    mulGrp 
↾s          mulGrp  ↾s          mulGrp  ↾s         |
50 | 44, 46, 49 | 3eqtr4d 2220 |
. . . . 5
          
  mulGrp 
↾s                
  mulGrp 
↾s               |
51 | | basfn 12522 |
. . . . . . . . . . . 12
 |
52 | 10 | elexd 2752 |
. . . . . . . . . . . 12
   |
53 | | funfvex 5534 |
. . . . . . . . . . . . 13
 
       |
54 | 53 | funfni 5318 |
. . . . . . . . . . . 12
 
       |
55 | 51, 52, 54 | sylancr 414 |
. . . . . . . . . . 11
       |
56 | 1, 55 | eqeltrid 2264 |
. . . . . . . . . 10
   |
57 | 56, 18 | ssexd 4145 |
. . . . . . . . 9
   |
58 | | ressex 12527 |
. . . . . . . . . 10
    ↾s    |
59 | | eqid 2177 |
. . . . . . . . . . 11
mulGrp 
↾s   mulGrp  ↾s    |
60 | | eqid 2177 |
. . . . . . . . . . 11
    ↾s       ↾s    |
61 | 59, 60 | mgpplusgg 13139 |
. . . . . . . . . 10
  ↾s      ↾s     mulGrp 
↾s      |
62 | 58, 61 | syl 14 |
. . . . . . . . 9
       ↾s     mulGrp  ↾s      |
63 | 10, 57, 62 | syl2anc 411 |
. . . . . . . 8
     ↾s     mulGrp 
↾s      |
64 | | eqid 2177 |
. . . . . . . . . 10
 ↾s   ↾s   |
65 | 64, 3 | ressmulrg 12605 |
. . . . . . . . 9
 
    
↾s     |
66 | 57, 10, 65 | syl2anc 411 |
. . . . . . . 8
     ↾s     |
67 | | eqid 2177 |
. . . . . . . . . . 11
mulGrp  mulGrp   |
68 | 64, 67 | mgpress 13146 |
. . . . . . . . . 10
    mulGrp  ↾s  mulGrp 
↾s     |
69 | 11, 57, 68 | syl2anc 411 |
. . . . . . . . 9
  mulGrp  ↾s  mulGrp 
↾s     |
70 | 69 | fveq2d 5521 |
. . . . . . . 8
    mulGrp  ↾s     mulGrp 
↾s      |
71 | 63, 66, 70 | 3eqtr4d 2220 |
. . . . . . 7
    mulGrp  ↾s     |
72 | 71 | oveqd 5894 |
. . . . . 6
        mulGrp  ↾s       |
73 | 72 | fveq2d 5521 |
. . . . 5
                    
  mulGrp 
↾s        |
74 | 71 | oveqd 5894 |
. . . . 5
         
                      mulGrp  ↾s               |
75 | 50, 73, 74 | 3eqtr4d 2220 |
. . . 4
                   
           |
76 | 75 | oveq2d 5893 |
. . 3
                                       |
77 | 1, 3 | ringcl 13201 |
. . . . 5
 
     |
78 | 11, 12, 23, 77 | syl3anc 1238 |
. . . 4
     |
79 | 5, 3 | unitmulcl 13287 |
. . . . 5
 
     |
80 | 11, 13, 24, 79 | syl3anc 1238 |
. . . 4
     |
81 | 2, 4, 6, 7, 9, 11,
78, 80 | dvrvald 13308 |
. . 3
                       |
82 | 5, 19 | unitinvcl 13297 |
. . . . . . . . 9
             |
83 | 11, 24, 82 | syl2anc 411 |
. . . . . . . 8
           |
84 | 18, 83 | sseldd 3158 |
. . . . . . 7
           |
85 | 1, 3 | ringass 13204 |
. . . . . . 7
  
                                    |
86 | 11, 12, 23, 84, 85 | syl13anc 1240 |
. . . . . 6
                           |
87 | 2, 4, 6, 7, 9, 11,
23, 24 | dvrvald 13308 |
. . . . . . 7
               |
88 | 87 | oveq2d 5893 |
. . . . . 6
      
            |
89 | 86, 88 | eqtr4d 2213 |
. . . . 5
                   |
90 | 89 | oveq1d 5892 |
. . . 4
             
           
             |
91 | 1, 3 | ringass 13204 |
. . . . 5
            
                                                        |
92 | 11, 78, 84, 22, 91 | syl13anc 1240 |
. . . 4
             
                                 |
93 | 1, 3 | ringass 13204 |
. . . . 5
  

                           
             |
94 | 11, 12, 26, 22, 93 | syl13anc 1240 |
. . . 4
   
              
            |
95 | 90, 92, 94 | 3eqtr3rd 2219 |
. . 3
    
                     
            |
96 | 76, 81, 95 | 3eqtr4rd 2221 |
. 2
    
             
    |
97 | 32, 96 | eqtrd 2210 |
1
          
    |