Step | Hyp | Ref
| Expression |
1 | | imasring.u |
. . . 4
  s    |
2 | | imasring.v |
. . . 4
       |
3 | | imasring.f |
. . . 4
       |
4 | | imasring.r |
. . . 4
   |
5 | 1, 2, 3, 4 | imasbas 15413 |
. . 3
       |
6 | | eqidd 2452 |
. . 3
         |
7 | | eqidd 2452 |
. . 3
           |
8 | | imasring.p |
. . . . . 6
    |
9 | 8 | a1i 11 |
. . . . 5
      |
10 | | imasring.e1 |
. . . . 5
 

 
 
                      
           |
11 | | ringgrp 17785 |
. . . . . 6

  |
12 | 4, 11 | syl 17 |
. . . . 5
   |
13 | | eqid 2451 |
. . . . 5
         |
14 | 1, 2, 9, 3, 10, 12, 13 | imasgrp 16802 |
. . . 4
                 |
15 | 14 | simpld 461 |
. . 3
   |
16 | | imasring.e2 |
. . . . 5
 

 
 
                      
           |
17 | | imasring.t |
. . . . 5
     |
18 | | eqid 2451 |
. . . . 5
         |
19 | 4 | adantr 467 |
. . . . . . . 8
 

 
  |
20 | | simprl 764 |
. . . . . . . . 9
 

 
  |
21 | 2 | adantr 467 |
. . . . . . . . 9
 

 
      |
22 | 20, 21 | eleqtrd 2531 |
. . . . . . . 8
 

 
      |
23 | | simprr 766 |
. . . . . . . . 9
 

    |
24 | 23, 21 | eleqtrd 2531 |
. . . . . . . 8
 

        |
25 | | eqid 2451 |
. . . . . . . . 9
         |
26 | 25, 17 | ringcl 17794 |
. . . . . . . 8
     
    
        |
27 | 19, 22, 24, 26 | syl3anc 1268 |
. . . . . . 7
 

          |
28 | 27, 21 | eleqtrrd 2532 |
. . . . . 6
 

      |
29 | 28 | caovclg 6461 |
. . . . 5
 

      |
30 | 3, 16, 1, 2, 4, 17,
18, 29 | imasmulf 15442 |
. . . 4
             |
31 | | fovrn 6439 |
. . . 4
           

          |
32 | 30, 31 | syl3an1 1301 |
. . 3
 

          |
33 | | forn 5796 |
. . . . . . . . . 10
       |
34 | 3, 33 | syl 17 |
. . . . . . . . 9
   |
35 | 34 | eleq2d 2514 |
. . . . . . . 8
     |
36 | 34 | eleq2d 2514 |
. . . . . . . 8
     |
37 | 34 | eleq2d 2514 |
. . . . . . . 8
     |
38 | 35, 36, 37 | 3anbi123d 1339 |
. . . . . . 7
  


    |
39 | | fofn 5795 |
. . . . . . . . 9
    
  |
40 | 3, 39 | syl 17 |
. . . . . . . 8
   |
41 | | fvelrnb 5912 |
. . . . . . . . 9
          |
42 | | fvelrnb 5912 |
. . . . . . . . 9
          |
43 | | fvelrnb 5912 |
. . . . . . . . 9
          |
44 | 41, 42, 43 | 3anbi123d 1339 |
. . . . . . . 8
     
                  |
45 | 40, 44 | syl 17 |
. . . . . . 7
  

 
   

             |
46 | 38, 45 | bitr3d 259 |
. . . . . 6
   
 
   

             |
47 | | 3reeanv 2959 |
. . . . . 6
  

             
 
   

            |
48 | 46, 47 | syl6bbr 267 |
. . . . 5
   



    
   
        |
49 | 4 | adantr 467 |
. . . . . . . . . . . . . 14
 

 
  |
50 | | simp2 1009 |
. . . . . . . . . . . . . . . 16
 

  |
51 | 2 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . 16
 

      |
52 | 50, 51 | eleqtrd 2531 |
. . . . . . . . . . . . . . 15
 

      |
53 | 52 | 3adant3r3 1219 |
. . . . . . . . . . . . . 14
 

 
      |
54 | | simp3 1010 |
. . . . . . . . . . . . . . . 16
 

  |
55 | 54, 51 | eleqtrd 2531 |
. . . . . . . . . . . . . . 15
 

      |
56 | 55 | 3adant3r3 1219 |
. . . . . . . . . . . . . 14
 

        |
57 | | simpr3 1016 |
. . . . . . . . . . . . . . 15
 

    |
58 | 2 | adantr 467 |
. . . . . . . . . . . . . . 15
 

 
      |
59 | 57, 58 | eleqtrd 2531 |
. . . . . . . . . . . . . 14
 

        |
60 | 25, 17 | ringass 17797 |
. . . . . . . . . . . . . 14
          
        
       |
61 | 49, 53, 56, 59, 60 | syl13anc 1270 |
. . . . . . . . . . . . 13
 

            |
62 | 61 | fveq2d 5869 |
. . . . . . . . . . . 12
 

       
            |
63 | | simpl 459 |
. . . . . . . . . . . . 13
 

    |
64 | 28 | caovclg 6461 |
. . . . . . . . . . . . . 14
 

      |
65 | 64 | 3adantr3 1169 |
. . . . . . . . . . . . 13
 

      |
66 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 15441 |
. . . . . . . . . . . . 13
 
 

                            |
67 | 63, 65, 57, 66 | syl3anc 1268 |
. . . . . . . . . . . 12
 

      
                       |
68 | | simpr1 1014 |
. . . . . . . . . . . . 13
 

 
  |
69 | 28 | caovclg 6461 |
. . . . . . . . . . . . . 14
 

      |
70 | 69 | 3adantr1 1167 |
. . . . . . . . . . . . 13
 

      |
71 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 15441 |
. . . . . . . . . . . . 13
 
  
                     
      |
72 | 63, 68, 70, 71 | syl3anc 1268 |
. . . . . . . . . . . 12
 

                              |
73 | 62, 67, 72 | 3eqtr4d 2495 |
. . . . . . . . . . 11
 

      
                           
     |
74 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 15441 |
. . . . . . . . . . . . 13
 

                   
    |
75 | 74 | 3adant3r3 1219 |
. . . . . . . . . . . 12
 

                          |
76 | 75 | oveq1d 6305 |
. . . . . . . . . . 11
 

                                                  |
77 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 15441 |
. . . . . . . . . . . . 13
 

                   
    |
78 | 77 | 3adant3r1 1217 |
. . . . . . . . . . . 12
 

                          |
79 | 78 | oveq2d 6306 |
. . . . . . . . . . 11
 

                                                  |
80 | 73, 76, 79 | 3eqtr4d 2495 |
. . . . . . . . . 10
 

                                                            |
81 | | simp1 1008 |
. . . . . . . . . . . . 13
                     |
82 | | simp2 1009 |
. . . . . . . . . . . . 13
                     |
83 | 81, 82 | oveq12d 6308 |
. . . . . . . . . . . 12
                                         |
84 | | simp3 1010 |
. . . . . . . . . . . 12
                     |
85 | 83, 84 | oveq12d 6308 |
. . . . . . . . . . 11
                                                             |
86 | 82, 84 | oveq12d 6308 |
. . . . . . . . . . . 12
                                         |
87 | 81, 86 | oveq12d 6308 |
. . . . . . . . . . 11
                                                             |
88 | 85, 87 | eqeq12d 2466 |
. . . . . . . . . 10
                                                                       
                                   |
89 | 80, 88 | syl5ibcom 224 |
. . . . . . . . 9
 

                                                    |
90 | 89 | 3exp2 1227 |
. . . . . . . 8
                                                         |
91 | 90 | imp32 435 |
. . . . . . 7
 

                                                      |
92 | 91 | rexlimdv 2877 |
. . . . . 6
 

                                                     |
93 | 92 | rexlimdvva 2886 |
. . . . 5
                                                      |
94 | 48, 93 | sylbid 219 |
. . . 4
                                       |
95 | 94 | imp 431 |
. . 3
 

                                    |
96 | 25, 8, 17 | ringdi 17799 |
. . . . . . . . . . . . . 14
          
      
      
    |
97 | 49, 53, 56, 59, 96 | syl13anc 1270 |
. . . . . . . . . . . . 13
 

   
          |
98 | 97 | fveq2d 5869 |
. . . . . . . . . . . 12
 

     
          
     |
99 | 25, 8 | ringacl 17808 |
. . . . . . . . . . . . . . . . 17
     
    
        |
100 | 19, 22, 24, 99 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
 

          |
101 | 100, 21 | eleqtrrd 2532 |
. . . . . . . . . . . . . . 15
 

      |
102 | 101 | caovclg 6461 |
. . . . . . . . . . . . . 14
 

      |
103 | 102 | 3adantr1 1167 |
. . . . . . . . . . . . 13
 

      |
104 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 15441 |
. . . . . . . . . . . . 13
 
  
                     
      |
105 | 63, 68, 103, 104 | syl3anc 1268 |
. . . . . . . . . . . 12
 

                              |
106 | 28 | caovclg 6461 |
. . . . . . . . . . . . . 14
 

      |
107 | 106 | 3adantr2 1168 |
. . . . . . . . . . . . 13
 

      |
108 | | eqid 2451 |
. . . . . . . . . . . . . 14
       |
109 | 3, 10, 1, 2, 4, 8, 108 | imasaddval 15438 |
. . . . . . . . . . . . 13
 
                    
               |
110 | 63, 65, 107, 109 | syl3anc 1268 |
. . . . . . . . . . . 12
 

      
          
               |
111 | 98, 105, 110 | 3eqtr4d 2495 |
. . . . . . . . . . 11
 

                                   
     |
112 | 3, 10, 1, 2, 4, 8, 108 | imasaddval 15438 |
. . . . . . . . . . . . 13
 

      
                |
113 | 112 | 3adant3r1 1217 |
. . . . . . . . . . . 12
 

                         |
114 | 113 | oveq2d 6306 |
. . . . . . . . . . 11
 

                                           
     |
115 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 15441 |
. . . . . . . . . . . . 13
 

                   
    |
116 | 115 | 3adant3r2 1218 |
. . . . . . . . . . . 12
 

                          |
117 | 75, 116 | oveq12d 6308 |
. . . . . . . . . . 11
 

                                                        
     |
118 | 111, 114,
117 | 3eqtr4d 2495 |
. . . . . . . . . 10
 

                                                                      |
119 | 82, 84 | oveq12d 6308 |
. . . . . . . . . . . 12
                                       |
120 | 81, 119 | oveq12d 6308 |
. . . . . . . . . . 11
                                                           |
121 | 81, 84 | oveq12d 6308 |
. . . . . . . . . . . 12
                                         |
122 | 83, 121 | oveq12d 6308 |
. . . . . . . . . . 11
                                                                               |
123 | 120, 122 | eqeq12d 2466 |
. . . . . . . . . 10
                                                                                 
                                         |
124 | 118, 123 | syl5ibcom 224 |
. . . . . . . . 9
 

                                                          |
125 | 124 | 3exp2 1227 |
. . . . . . . 8
                                                               |
126 | 125 | imp32 435 |
. . . . . . 7
 

                                                            |
127 | 126 | rexlimdv 2877 |
. . . . . 6
 

                                                           |
128 | 127 | rexlimdvva 2886 |
. . . . 5
                                                            |
129 | 48, 128 | sylbid 219 |
. . . 4
                                             |
130 | 129 | imp 431 |
. . 3
 

                                          |
131 | 25, 8, 17 | ringdir 17800 |
. . . . . . . . . . . . . 14
          
        
         |
132 | 49, 53, 56, 59, 131 | syl13anc 1270 |
. . . . . . . . . . . . 13
 

              |
133 | 132 | fveq2d 5869 |
. . . . . . . . . . . 12
 

       
              |
134 | 101 | caovclg 6461 |
. . . . . . . . . . . . . 14
 

      |
135 | 134 | 3adantr3 1169 |
. . . . . . . . . . . . 13
 

      |
136 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 15441 |
. . . . . . . . . . . . 13
 
 

                            |
137 | 63, 135, 57, 136 | syl3anc 1268 |
. . . . . . . . . . . 12
 

      
                       |
138 | 3, 10, 1, 2, 4, 8, 108 | imasaddval 15438 |
. . . . . . . . . . . . 13
 
                    
               |
139 | 63, 107, 70, 138 | syl3anc 1268 |
. . . . . . . . . . . 12
 

      
                   
      |
140 | 133, 137,
139 | 3eqtr4d 2495 |
. . . . . . . . . . 11
 

      
                            
     |
141 | 3, 10, 1, 2, 4, 8, 108 | imasaddval 15438 |
. . . . . . . . . . . . 13
 

      
                |
142 | 141 | 3adant3r3 1219 |
. . . . . . . . . . . 12
 

                    
    |
143 | 142 | oveq1d 6305 |
. . . . . . . . . . 11
 

                                                 |
144 | 116, 78 | oveq12d 6308 |
. . . . . . . . . . 11
 

                                                        
     |
145 | 140, 143,
144 | 3eqtr4d 2495 |
. . . . . . . . . 10
 

                                                                      |
146 | 81, 82 | oveq12d 6308 |
. . . . . . . . . . . 12
                                       |
147 | 146, 84 | oveq12d 6308 |
. . . . . . . . . . 11
                                                           |
148 | 121, 86 | oveq12d 6308 |
. . . . . . . . . . 11
                                                                               |
149 | 147, 148 | eqeq12d 2466 |
. . . . . . . . . 10
                                                                                 
                                         |
150 | 145, 149 | syl5ibcom 224 |
. . . . . . . . 9
 

                                                          |
151 | 150 | 3exp2 1227 |
. . . . . . . 8
                                                               |
152 | 151 | imp32 435 |
. . . . . . 7
 

                                                            |
153 | 152 | rexlimdv 2877 |
. . . . . 6
 

                                                           |
154 | 153 | rexlimdvva 2886 |
. . . . 5
                                                            |
155 | 48, 154 | sylbid 219 |
. . . 4
                                             |
156 | 155 | imp 431 |
. . 3
 

                                          |
157 | | fof 5793 |
. . . . 5
           |
158 | 3, 157 | syl 17 |
. . . 4
       |
159 | | imasring.o |
. . . . . . 7
     |
160 | 25, 159 | ringidcl 17801 |
. . . . . 6

      |
161 | 4, 160 | syl 17 |
. . . . 5
       |
162 | 161, 2 | eleqtrrd 2532 |
. . . 4
   |
163 | 158, 162 | ffvelrnd 6023 |
. . 3
  
  |
164 | 40, 41 | syl 17 |
. . . . . 6
  
       |
165 | 35, 164 | bitr3d 259 |
. . . . 5
          |
166 | | simpl 459 |
. . . . . . . . 9
 
   |
167 | 162 | adantr 467 |
. . . . . . . . 9
 
   |
168 | | simpr 463 |
. . . . . . . . 9
 
   |
169 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 15441 |
. . . . . . . . 9
 

                     |
170 | 166, 167,
168, 169 | syl3anc 1268 |
. . . . . . . 8
 
                 
    |
171 | 4 | adantr 467 |
. . . . . . . . . 10
 
   |
172 | 2 | eleq2d 2514 |
. . . . . . . . . . 11
         |
173 | 172 | biimpa 487 |
. . . . . . . . . 10
 
       |
174 | 25, 17, 159 | ringlidm 17804 |
. . . . . . . . . 10
          |
175 | 171, 173,
174 | syl2anc 667 |
. . . . . . . . 9
 
    |
176 | 175 | fveq2d 5869 |
. . . . . . . 8
 
            |
177 | 170, 176 | eqtrd 2485 |
. . . . . . 7
 
                     |
178 | | oveq2 6298 |
. . . . . . . 8
                               |
179 | | id 22 |
. . . . . . . 8
           |
180 | 178, 179 | eqeq12d 2466 |
. . . . . . 7
                       
             |
181 | 177, 180 | syl5ibcom 224 |
. . . . . 6
 
                   |
182 | 181 | rexlimdva 2879 |
. . . . 5
                    |
183 | 165, 182 | sylbid 219 |
. . . 4
               |
184 | 183 | imp 431 |
. . 3
 
             |
185 | 3, 16, 1, 2, 4, 17,
18 | imasmulval 15441 |
. . . . . . . . 9
 

                 
   |
186 | 167, 185 | mpd3an3 1365 |
. . . . . . . 8
 
                  
   |
187 | 25, 17, 159 | ringridm 17805 |
. . . . . . . . . 10
       
  |
188 | 171, 173,
187 | syl2anc 667 |
. . . . . . . . 9
 
 
  |
189 | 188 | fveq2d 5869 |
. . . . . . . 8
 
            |
190 | 186, 189 | eqtrd 2485 |
. . . . . . 7
 
                     |
191 | | oveq1 6297 |
. . . . . . . 8
                               |
192 | 191, 179 | eqeq12d 2466 |
. . . . . . 7
                       
             |
193 | 190, 192 | syl5ibcom 224 |
. . . . . 6
 
                   |
194 | 193 | rexlimdva 2879 |
. . . . 5
                    |
195 | 165, 194 | sylbid 219 |
. . . 4
               |
196 | 195 | imp 431 |
. . 3
 
             |
197 | 5, 6, 7, 15, 32, 95, 130, 156, 163, 184, 196 | isringd 17815 |
. 2
   |
198 | 163, 5 | eleqtrd 2531 |
. . . 4
  
      |
199 | 5 | eleq2d 2514 |
. . . . . 6
         |
200 | 183, 195 | jcad 536 |
. . . . . 6
                           |
201 | 199, 200 | sylbird 239 |
. . . . 5
                               |
202 | 201 | ralrimiv 2800 |
. . . 4
                               |
203 | | eqid 2451 |
. . . . . 6
         |
204 | | eqid 2451 |
. . . . . 6
         |
205 | 203, 18, 204 | isringid 17806 |
. . . . 5

   
    
                                     |
206 | 197, 205 | syl 17 |
. . . 4
        
                            
         |
207 | 198, 202,
206 | mpbi2and 932 |
. . 3
         |
208 | 207 | eqcomd 2457 |
. 2
  
      |
209 | 197, 208 | jca 535 |
1
   
       |