Step | Hyp | Ref
| Expression |
1 | | oveq1 5875 |
. . . . . . . 8
 
     |
2 | 1 | oveq1d 5883 |
. . . . . . 7
   
       |
3 | | oveq1 5875 |
. . . . . . 7
 
         |
4 | 2, 3 | eqeq12d 2192 |
. . . . . 6
         
 
         |
5 | 4 | imbi2d 230 |
. . . . 5
      SRing
 
         

SRing             |
6 | | oveq1 5875 |
. . . . . . . 8
 
     |
7 | 6 | oveq1d 5883 |
. . . . . . 7
   
       |
8 | | oveq1 5875 |
. . . . . . 7
 
         |
9 | 7, 8 | eqeq12d 2192 |
. . . . . 6
         
 
         |
10 | 9 | imbi2d 230 |
. . . . 5
      SRing
 
         

SRing             |
11 | | oveq1 5875 |
. . . . . . . 8
   
       |
12 | 11 | oveq1d 5883 |
. . . . . . 7
     
         |
13 | | oveq1 5875 |
. . . . . . 7
   
           |
14 | 12, 13 | eqeq12d 2192 |
. . . . . 6
           
               |
15 | 14 | imbi2d 230 |
. . . . 5
        SRing
 
         

SRing                 |
16 | | oveq1 5875 |
. . . . . . . 8
 
     |
17 | 16 | oveq1d 5883 |
. . . . . . 7
   
       |
18 | | oveq1 5875 |
. . . . . . 7
 
         |
19 | 17, 18 | eqeq12d 2192 |
. . . . . 6
         
           |
20 | 19 | imbi2d 230 |
. . . . 5
      SRing
 
         

SRing             |
21 | | simpr 110 |
. . . . . . 7
  

SRing SRing |
22 | | simpr 110 |
. . . . . . . 8
 
   |
23 | 22 | adantr 276 |
. . . . . . 7
  

SRing   |
24 | | srgmulgass.b |
. . . . . . . 8
     |
25 | | srgmulgass.t |
. . . . . . . 8
     |
26 | | eqid 2177 |
. . . . . . . 8
         |
27 | 24, 25, 26 | srglz 12981 |
. . . . . . 7
  SRing
     
       |
28 | 21, 23, 27 | syl2anc 411 |
. . . . . 6
  

SRing             |
29 | | simpl 109 |
. . . . . . . . 9
 
   |
30 | 29 | adantr 276 |
. . . . . . . 8
  

SRing   |
31 | | srgmulgass.m |
. . . . . . . . 9
.g   |
32 | 24, 26, 31 | mulg0 12864 |
. . . . . . . 8
 
       |
33 | 30, 32 | syl 14 |
. . . . . . 7
  

SRing         |
34 | 33 | oveq1d 5883 |
. . . . . 6
  

SRing         
   |
35 | 24, 25 | srgcl 12966 |
. . . . . . . 8
  SRing
     |
36 | 21, 30, 23, 35 | syl3anc 1238 |
. . . . . . 7
  

SRing     |
37 | 24, 26, 31 | mulg0 12864 |
. . . . . . 7
 

          |
38 | 36, 37 | syl 14 |
. . . . . 6
  

SRing           |
39 | 28, 34, 38 | 3eqtr4d 2220 |
. . . . 5
  

SRing           |
40 | | srgmnd 12963 |
. . . . . . . . . . . . . 14
 SRing   |
41 | 40 | adantl 277 |
. . . . . . . . . . . . 13
  

SRing   |
42 | 41 | adantl 277 |
. . . . . . . . . . . 12
     SRing   |
43 | | simpl 109 |
. . . . . . . . . . . 12
     SRing   |
44 | 30 | adantl 277 |
. . . . . . . . . . . 12
     SRing   |
45 | | eqid 2177 |
. . . . . . . . . . . . 13
       |
46 | 24, 31, 45 | mulgnn0p1 12870 |
. . . . . . . . . . . 12
 
                |
47 | 42, 43, 44, 46 | syl3anc 1238 |
. . . . . . . . . . 11
     SRing                |
48 | 47 | oveq1d 5883 |
. . . . . . . . . 10
     SRing     
              |
49 | 21 | adantl 277 |
. . . . . . . . . . 11
     SRing SRing |
50 | 24, 31 | mulgnn0cl 12875 |
. . . . . . . . . . . 12
 
 
   |
51 | 42, 43, 44, 50 | syl3anc 1238 |
. . . . . . . . . . 11
     SRing 
   |
52 | 23 | adantl 277 |
. . . . . . . . . . 11
     SRing   |
53 | 24, 45, 25 | srgdir 12971 |
. . . . . . . . . . 11
  SRing
  
 
                          |
54 | 49, 51, 44, 52, 53 | syl13anc 1240 |
. . . . . . . . . 10
     SRing                           |
55 | 48, 54 | eqtrd 2210 |
. . . . . . . . 9
     SRing     
                |
56 | 55 | adantr 276 |
. . . . . . . 8
      SRing   
  
       
                |
57 | | oveq1 5875 |
. . . . . . . . 9
   
  
 
   
  
                     |
58 | 35 | 3expb 1204 |
. . . . . . . . . . . . 13
  SRing

 
    |
59 | 58 | ancoms 268 |
. . . . . . . . . . . 12
  

SRing     |
60 | 59 | adantl 277 |
. . . . . . . . . . 11
     SRing     |
61 | 24, 31, 45 | mulgnn0p1 12870 |
. . . . . . . . . . 11
 
                        |
62 | 42, 43, 60, 61 | syl3anc 1238 |
. . . . . . . . . 10
     SRing                      |
63 | 62 | eqcomd 2183 |
. . . . . . . . 9
     SRing                      |
64 | 57, 63 | sylan9eqr 2232 |
. . . . . . . 8
      SRing   
  
                        |
65 | 56, 64 | eqtrd 2210 |
. . . . . . 7
      SRing   
  
       
    
    |
66 | 65 | exp31 364 |
. . . . . 6

  

SRing                          |
67 | 66 | a2d 26 |
. . . . 5

     SRing
 
      
  

SRing                 |
68 | 5, 10, 15, 20, 39, 67 | nn0ind 9343 |
. . . 4

  

SRing            |
69 | 68 | expd 258 |
. . 3

 
  SRing   
  
      |
70 | 69 | 3impib 1201 |
. 2
 
  SRing   
  
     |
71 | 70 | impcom 125 |
1
  SRing

            |