Step | Hyp | Ref
| Expression |
1 | | isdivrng1.1 |
. . 3
     |
2 | | isdivrng1.2 |
. . 3
     |
3 | | isdivrng1.3 |
. . 3
GId   |
4 | | isdivrng1.4 |
. . 3
 |
5 | 1, 2, 3, 4 | isdrngo1 32207 |
. 2
  
              |
6 | | isdivrng2.5 |
. . . . . . 7
GId   |
7 | 1, 2, 4, 3, 6 | dvrunz 26173 |
. . . . . 6
   |
8 | 5, 7 | sylbir 217 |
. . . . 5
              
  |
9 | | grporndm 25950 |
. . . . . . . . . . . 12
 
          
                          |
10 | 9 | adantl 468 |
. . . . . . . . . . 11
              
           
              |
11 | | difss 3562 |
. . . . . . . . . . . . . . . . 17
   
 |
12 | | xpss12 4943 |
. . . . . . . . . . . . . . . . 17
          
              |
13 | 11, 11, 12 | mp2an 679 |
. . . . . . . . . . . . . . . 16
             |
14 | 1, 2, 4 | rngosm 26121 |
. . . . . . . . . . . . . . . . 17
         |
15 | | fdm 5738 |
. . . . . . . . . . . . . . . . 17
           |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . 16


   |
17 | 13, 16 | syl5sseqr 3483 |
. . . . . . . . . . . . . . 15
             |
18 | 17 | adantr 467 |
. . . . . . . . . . . . . 14
              
            |
19 | | ssdmres 5129 |
. . . . . . . . . . . . . 14
                                   |
20 | 18, 19 | sylib 200 |
. . . . . . . . . . . . 13
              
                        |
21 | 20 | dmeqd 5040 |
. . . . . . . . . . . 12
              

                       |
22 | | dmxpid 5057 |
. . . . . . . . . . . 12
               |
23 | 21, 22 | syl6eq 2503 |
. . . . . . . . . . 11
              

                 |
24 | 10, 23 | eqtrd 2487 |
. . . . . . . . . 10
              
                  |
25 | 24 | eleq2d 2516 |
. . . . . . . . 9
              
                    |
26 | 25 | biimpar 488 |
. . . . . . . 8
   
           
    
              |
27 | | eqid 2453 |
. . . . . . . . . . 11
                         |
28 | | eqid 2453 |
. . . . . . . . . . 11
                                 |
29 | 27, 28 | grpoinvcl 25966 |
. . . . . . . . . 10
              
                                              |
30 | 29 | adantll 721 |
. . . . . . . . 9
   
           
            
                                  |
31 | | eqid 2453 |
. . . . . . . . . . . 12
GId 
            GId               |
32 | 27, 31, 28 | grpolinv 25968 |
. . . . . . . . . . 11
              
                                                GId 
              |
33 | 32 | adantll 721 |
. . . . . . . . . 10
   
           
            
                      
             GId 
              |
34 | 2 | rngomndo 26161 |
. . . . . . . . . . . . . 14
 MndOp |
35 | | mndomgmid 26082 |
. . . . . . . . . . . . . 14
 MndOp 
  |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . 13
 
  |
37 | 36 | adantr 467 |
. . . . . . . . . . . 12
              

  |
38 | 11, 4 | sseqtri 3466 |
. . . . . . . . . . . . . 14
   
 |
39 | 2, 1 | rngorn1eq 26160 |
. . . . . . . . . . . . . 14

  |
40 | 38, 39 | syl5sseq 3482 |
. . . . . . . . . . . . 13
       |
41 | 40 | adantr 467 |
. . . . . . . . . . . 12
              
   
  |
42 | 1 | rneqi 5064 |
. . . . . . . . . . . . . . . 16
     |
43 | 4, 42 | eqtri 2475 |
. . . . . . . . . . . . . . 15
     |
44 | 43, 2, 6 | rngo1cl 26169 |
. . . . . . . . . . . . . 14
   |
45 | 44 | adantr 467 |
. . . . . . . . . . . . 13
              
  |
46 | | eldifsn 4100 |
. . . . . . . . . . . . 13
    

   |
47 | 45, 8, 46 | sylanbrc 671 |
. . . . . . . . . . . 12
              
      |
48 | | grpomndo 26086 |
. . . . . . . . . . . . . 14
 
                       MndOp |
49 | | mndoismgmOLD 26081 |
. . . . . . . . . . . . . 14
 
           MndOp               |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . 13
 
                         |
51 | 50 | adantl 468 |
. . . . . . . . . . . 12
              
              |
52 | | eqid 2453 |
. . . . . . . . . . . . 13
 |
53 | | eqid 2453 |
. . . . . . . . . . . . 13
                         |
54 | 52, 6, 53 | exidresid 32189 |
. . . . . . . . . . . 12
   

        
           
GId 
              |
55 | 37, 41, 47, 51, 54 | syl31anc 1272 |
. . . . . . . . . . 11
              
GId 
              |
56 | 55 | adantr 467 |
. . . . . . . . . 10
   
           
            
GId                |
57 | 33, 56 | eqtrd 2487 |
. . . . . . . . 9
   
           
            
                      
               |
58 | | oveq1 6302 |
. . . . . . . . . . 11
                                                           
               |
59 | 58 | eqeq1d 2455 |
. . . . . . . . . 10
                        
            
                      
                |
60 | 59 | rspcev 3152 |
. . . . . . . . 9
                                                                        
                              |
61 | 30, 57, 60 | syl2anc 667 |
. . . . . . . 8
   
           
            
                                |
62 | 26, 61 | syldan 473 |
. . . . . . 7
   
           
     

                              |
63 | 24 | adantr 467 |
. . . . . . . . 9
   
           
                       |
64 | 63 | rexeqdv 2996 |
. . . . . . . 8
   
           
                                    
       
                |
65 | | ovres 6441 |
. . . . . . . . . . . 12
     

                          |
66 | 65 | ancoms 455 |
. . . . . . . . . . 11
     

                          |
67 | 66 | eqeq1d 2455 |
. . . . . . . . . 10
     

       
            
       |
68 | 67 | rexbidva 2900 |
. . . . . . . . 9
                           
             |
69 | 68 | adantl 468 |
. . . . . . . 8
   
           
                           
             |
70 | 64, 69 | bitrd 257 |
. . . . . . 7
   
           
                                    
            |
71 | 62, 70 | mpbid 214 |
. . . . . 6
   
           
     
           |
72 | 71 | ralrimiva 2804 |
. . . . 5
              
                  |
73 | 8, 72 | jca 535 |
. . . 4
              
 
                  |
74 | | fvex 5880 |
. . . . . . . . 9
     |
75 | 1, 74 | eqeltri 2527 |
. . . . . . . 8
 |
76 | 75 | rnex 6732 |
. . . . . . 7
 |
77 | 4, 76 | eqeltri 2527 |
. . . . . 6
 |
78 | | difexg 4554 |
. . . . . 6
       |
79 | 77, 78 | mp1i 13 |
. . . . 5
   
                       |
80 | | ffn 5733 |
. . . . . . . . 9
      
    |
81 | 14, 80 | syl 17 |
. . . . . . . 8
     |
82 | 81 | adantr 467 |
. . . . . . 7
   
                
    |
83 | | fnssres 5694 |
. . . . . . 7
              
                          |
84 | 82, 13, 83 | sylancl 669 |
. . . . . 6
   
                                         |
85 | | ovres 6441 |
. . . . . . . . 9
     

                          |
86 | 85 | adantl 468 |
. . . . . . . 8
   
                  
   

       
                   |
87 | | eldifi 3557 |
. . . . . . . . . . . 12
    
  |
88 | | eldifi 3557 |
. . . . . . . . . . . 12
       |
89 | 87, 88 | anim12i 570 |
. . . . . . . . . . 11
     

    
   |
90 | 1, 2, 4 | rngocl 26122 |
. . . . . . . . . . . 12
 
       |
91 | 90 | 3expb 1210 |
. . . . . . . . . . 11
  
 
      |
92 | 89, 91 | sylan2 477 |
. . . . . . . . . 10
      

           |
93 | 92 | adantlr 722 |
. . . . . . . . 9
   
                  
   

           |
94 | | oveq2 6303 |
. . . . . . . . . . . . . . . 16
           |
95 | 94 | eqeq1d 2455 |
. . . . . . . . . . . . . . 15
     
       |
96 | 95 | rexbidv 2903 |
. . . . . . . . . . . . . 14
  
         
            |
97 | 96 | rspcv 3148 |
. . . . . . . . . . . . 13
                     
             |
98 | 97 | imdistanri 698 |
. . . . . . . . . . . 12
                                         |
99 | | eldifsn 4100 |
. . . . . . . . . . . . . . 15
    

   |
100 | | ssrexv 3496 |
. . . . . . . . . . . . . . . . . . . . . 22
               

       |
101 | 11, 100 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
                  |
102 | 1, 2, 3, 4, 6 | zerdivemp1x 32206 |
. . . . . . . . . . . . . . . . . . . . 21
 

               |
103 | 101, 102 | syl3an3 1304 |
. . . . . . . . . . . . . . . . . . . 20
 
                     |
104 | 87, 103 | syl3an2 1303 |
. . . . . . . . . . . . . . . . . . 19
      
          
         |
105 | 104 | 3expb 1210 |
. . . . . . . . . . . . . . . . . 18
      
                      |
106 | 105 | imp 431 |
. . . . . . . . . . . . . . . . 17
   
   
           
         |
107 | 106 | necon3d 2647 |
. . . . . . . . . . . . . . . 16
   
   
           
         |
108 | 107 | impr 625 |
. . . . . . . . . . . . . . 15
   
   
            
        |
109 | 99, 108 | sylan2b 478 |
. . . . . . . . . . . . . 14
   
   
           
    
      |
110 | 109 | an32s 814 |
. . . . . . . . . . . . 13
  
                            |
111 | 110 | ancom2s 812 |
. . . . . . . . . . . 12
  
                            |
112 | 98, 111 | sylan2 477 |
. . . . . . . . . . 11
  
      
                           |
113 | 112 | an42s 837 |
. . . . . . . . . 10
                        

           |
114 | 113 | adantlrl 727 |
. . . . . . . . 9
   
                  
   

           |
115 | | eldifsn 4100 |
. . . . . . . . 9
        
            |
116 | 93, 114, 115 | sylanbrc 671 |
. . . . . . . 8
   
                  
   

               |
117 | 86, 116 | eqeltrd 2531 |
. . . . . . 7
   
                  
   

       
                   |
118 | 117 | ralrimivva 2811 |
. . . . . 6
   
                 
                                 |
119 | | ffnov 6405 |
. . . . . 6
 
                            
                                                          |
120 | 84, 118, 119 | sylanbrc 671 |
. . . . 5
   
                                                 |
121 | 116 | 3adantr3 1170 |
. . . . . . 7
   
                  
   

                   |
122 | | simpr3 1017 |
. . . . . . 7
   
                  
   

               |
123 | 121, 122 | ovresd 6442 |
. . . . . 6
   
                  
   

               
                       |
124 | 85 | 3adant3 1029 |
. . . . . . . 8
     

                              |
125 | 124 | adantl 468 |
. . . . . . 7
   
                  
   

           
                   |
126 | 125 | oveq1d 6310 |
. . . . . 6
   
                  
   

                                                               |
127 | | ovres 6441 |
. . . . . . . . . 10
     

                          |
128 | 127 | 3adant1 1027 |
. . . . . . . . 9
     

                              |
129 | 128 | adantl 468 |
. . . . . . . 8
   
                  
   

           
                   |
130 | 129 | oveq2d 6311 |
. . . . . . 7
   
                  
   

                                       |
131 | | simpr1 1015 |
. . . . . . . 8
   
                  
   

               |
132 | | fovrn 6444 |
. . . . . . . . . 10
                                                               |
133 | 132 | 3adant3r1 1218 |
. . . . . . . . 9
                                    

           
                   |
134 | 120, 133 | sylan 474 |
. . . . . . . 8
   
                  
   

           
                   |
135 | 131, 134 | ovresd 6442 |
. . . . . . 7
   
                  
   

           
                                                   |
136 | | eldifi 3557 |
. . . . . . . . . 10
    
  |
137 | 87, 88, 136 | 3anim123i 1194 |
. . . . . . . . 9
     

        
   |
138 | 1, 2, 4 | rngoass 26127 |
. . . . . . . . 9
  
 
                  |
139 | 137, 138 | sylan2 477 |
. . . . . . . 8
      

                           |
140 | 139 | adantlr 722 |
. . . . . . 7
   
                  
   

                           |
141 | 130, 135,
140 | 3eqtr4d 2497 |
. . . . . 6
   
                  
   

           
                                       |
142 | 123, 126,
141 | 3eqtr4d 2497 |
. . . . 5
   
                  
   

                                                                           |
143 | 44 | anim1i 572 |
. . . . . . 7
   
   |
144 | 143, 46 | sylibr 216 |
. . . . . 6
         |
145 | 144 | adantrr 724 |
. . . . 5
   
                
      |
146 | | ovres 6441 |
. . . . . . . 8
     

                          |
147 | 144, 146 | sylan 474 |
. . . . . . 7
   
    
                      |
148 | 2, 43, 6 | rngolidm 26164 |
. . . . . . . . 9
         |
149 | 87, 148 | sylan2 477 |
. . . . . . . 8
             |
150 | 149 | adantlr 722 |
. . . . . . 7
   
    
      |
151 | 147, 150 | eqtrd 2487 |
. . . . . 6
   
    
                  |
152 | 151 | adantlrr 728 |
. . . . 5
   
                 
    
                  |
153 | 96 | rspcva 3150 |
. . . . . . . . 9
     
                             |
154 | | oveq1 6302 |
. . . . . . . . . . . 12
           |
155 | 154 | eqeq1d 2455 |
. . . . . . . . . . 11
     
       |
156 | 155 | cbvrexv 3022 |
. . . . . . . . . 10
           
           |
157 | | ovres 6441 |
. . . . . . . . . . . . . 14
     

                          |
158 | 157 | eqeq1d 2455 |
. . . . . . . . . . . . 13
     

       
            
       |
159 | 158 | ancoms 455 |
. . . . . . . . . . . 12
     

       
            
       |
160 | 159 | rexbidva 2900 |
. . . . . . . . . . 11
                           
             |
161 | 160 | biimpar 488 |
. . . . . . . . . 10
     
                                   |
162 | 156, 161 | sylan2b 478 |
. . . . . . . . 9
     
                                   |
163 | 153, 162 | syldan 473 |
. . . . . . . 8
     
                                         |
164 | 163 | ancoms 455 |
. . . . . . 7
                       
       
               |
165 | 164 | adantll 721 |
. . . . . 6
                         
       
               |
166 | 165 | adantlrl 727 |
. . . . 5
   
                 
    
                        |
167 | 79, 120, 142, 145, 152, 166 | isgrpda 26037 |
. . . 4
   
                               |
168 | 73, 167 | impbida 844 |
. . 3
                                   |
169 | 168 | pm5.32i 643 |
. 2
              
 
                    |
170 | 5, 169 | bitri 253 |
1
  
                    |