Step | Hyp | Ref
| Expression |
1 | | srgpcomp.k |
. 2
   |
2 | | oveq1 5875 |
. . . . . 6
 
     |
3 | 2 | oveq1d 5883 |
. . . . 5
   
       |
4 | 2 | oveq2d 5884 |
. . . . 5
      
    |
5 | 3, 4 | eqeq12d 2192 |
. . . 4
         
 
  
      |
6 | 5 | imbi2d 230 |
. . 3
  
 
  
    
 
  
       |
7 | | oveq1 5875 |
. . . . . 6
 
     |
8 | 7 | oveq1d 5883 |
. . . . 5
   
       |
9 | 7 | oveq2d 5884 |
. . . . 5
      
    |
10 | 8, 9 | eqeq12d 2192 |
. . . 4
         
 
  
      |
11 | 10 | imbi2d 230 |
. . 3
  
 
  
    
 
  
       |
12 | | oveq1 5875 |
. . . . . 6
   
       |
13 | 12 | oveq1d 5883 |
. . . . 5
     
         |
14 | 12 | oveq2d 5884 |
. . . . 5
          
    |
15 | 13, 14 | eqeq12d 2192 |
. . . 4
           
   
  
        |
16 | 15 | imbi2d 230 |
. . 3
    
 
  
    
   
  
         |
17 | | oveq1 5875 |
. . . . . 6
 
     |
18 | 17 | oveq1d 5883 |
. . . . 5
   
       |
19 | 17 | oveq2d 5884 |
. . . . 5
           |
20 | 18, 19 | eqeq12d 2192 |
. . . 4
         
    
      |
21 | 20 | imbi2d 230 |
. . 3
  
 
  
    
 
  
       |
22 | | srgpcomp.b |
. . . . . . . 8
   |
23 | | srgpcomp.r |
. . . . . . . . 9
 SRing |
24 | | srgpcomp.g |
. . . . . . . . . 10
mulGrp   |
25 | | srgpcomp.s |
. . . . . . . . . 10
     |
26 | 24, 25 | mgpbasg 12950 |
. . . . . . . . 9
 SRing       |
27 | 23, 26 | syl 14 |
. . . . . . . 8
       |
28 | 22, 27 | eleqtrd 2256 |
. . . . . . 7
       |
29 | | eqid 2177 |
. . . . . . . 8
         |
30 | | eqid 2177 |
. . . . . . . 8
         |
31 | | srgpcomp.e |
. . . . . . . 8
.g   |
32 | 29, 30, 31 | mulg0 12864 |
. . . . . . 7
    
        |
33 | 28, 32 | syl 14 |
. . . . . 6
         |
34 | | eqid 2177 |
. . . . . . . 8
         |
35 | 24, 34 | ringidvalg 12957 |
. . . . . . 7
 SRing           |
36 | 23, 35 | syl 14 |
. . . . . 6
           |
37 | 33, 36 | eqtr4d 2213 |
. . . . 5
         |
38 | 37 | oveq1d 5883 |
. . . 4
             |
39 | | srgpcomp.a |
. . . . . 6
   |
40 | | srgpcomp.m |
. . . . . . 7
     |
41 | 25, 40, 34 | srgridm 12976 |
. . . . . 6
  SRing
         |
42 | 23, 39, 41 | syl2anc 411 |
. . . . 5
         |
43 | 37 | oveq2d 5884 |
. . . . 5
  
          |
44 | 25, 40, 34 | srglidm 12975 |
. . . . . 6
  SRing
     
   |
45 | 23, 39, 44 | syl2anc 411 |
. . . . 5
         |
46 | 42, 43, 45 | 3eqtr4rd 2221 |
. . . 4
             |
47 | 38, 46 | eqtrd 2210 |
. . 3
           |
48 | 24 | srgmgp 12964 |
. . . . . . . . . . . . . 14
 SRing   |
49 | 23, 48 | syl 14 |
. . . . . . . . . . . . 13
   |
50 | 49 | adantr 276 |
. . . . . . . . . . . 12
 

  |
51 | | simpr 110 |
. . . . . . . . . . . 12
 

  |
52 | 22 | adantr 276 |
. . . . . . . . . . . . 13
 

  |
53 | 27 | adantr 276 |
. . . . . . . . . . . . 13
 

      |
54 | 52, 53 | eleqtrd 2256 |
. . . . . . . . . . . 12
 

      |
55 | | eqid 2177 |
. . . . . . . . . . . . 13
       |
56 | 29, 31, 55 | mulgnn0p1 12870 |
. . . . . . . . . . . 12
 
       
            |
57 | 50, 51, 54, 56 | syl3anc 1238 |
. . . . . . . . . . 11
 

               |
58 | 24, 40 | mgpplusgg 12948 |
. . . . . . . . . . . . . . 15
 SRing
     |
59 | 23, 58 | syl 14 |
. . . . . . . . . . . . . 14
      |
60 | 59 | oveqd 5885 |
. . . . . . . . . . . . 13
      
  
      |
61 | 60 | eqeq2d 2189 |
. . . . . . . . . . . 12
        
   
             |
62 | 61 | adantr 276 |
. . . . . . . . . . 11
 

   
    
                |
63 | 57, 62 | mpbird 167 |
. . . . . . . . . 10
 

          |
64 | 63 | oveq1d 5883 |
. . . . . . . . 9
 

   
      
   |
65 | | srgpcomp.c |
. . . . . . . . . . . . 13
       |
66 | 65 | eqcomd 2183 |
. . . . . . . . . . . 12
       |
67 | 66 | adantr 276 |
. . . . . . . . . . 11
 

  
   |
68 | 67 | oveq2d 5884 |
. . . . . . . . . 10
 

 
      
     |
69 | 23 | adantr 276 |
. . . . . . . . . . 11
 

SRing |
70 | 29, 31 | mulgnn0cl 12875 |
. . . . . . . . . . . . 13
 
     
       |
71 | 50, 51, 54, 70 | syl3anc 1238 |
. . . . . . . . . . . 12
 

        |
72 | 71, 53 | eleqtrrd 2257 |
. . . . . . . . . . 11
 

    |
73 | 39 | adantr 276 |
. . . . . . . . . . 11
 

  |
74 | 25, 40 | srgass 12967 |
. . . . . . . . . . 11
  SRing
  
 
   
    
     |
75 | 69, 72, 52, 73, 74 | syl13anc 1240 |
. . . . . . . . . 10
 

   
    
     |
76 | 25, 40 | srgass 12967 |
. . . . . . . . . . 11
  SRing
  
 
   
    
     |
77 | 69, 72, 73, 52, 76 | syl13anc 1240 |
. . . . . . . . . 10
 

   
    
     |
78 | 68, 75, 77 | 3eqtr4d 2220 |
. . . . . . . . 9
 

   
      
   |
79 | 64, 78 | eqtrd 2210 |
. . . . . . . 8
 

   
      
   |
80 | 79 | adantr 276 |
. . . . . . 7
      
               
    |
81 | | oveq1 5875 |
. . . . . . . 8
   
         
         |
82 | 25, 40 | srgass 12967 |
. . . . . . . . . 10
  SRing

 
 
      
 
     |
83 | 69, 73, 72, 52, 82 | syl13anc 1240 |
. . . . . . . . 9
 

      
 
     |
84 | 63 | eqcomd 2183 |
. . . . . . . . . 10
 

 
    
   |
85 | 84 | oveq2d 5884 |
. . . . . . . . 9
 

      
       |
86 | 83, 85 | eqtrd 2210 |
. . . . . . . 8
 

      
       |
87 | 81, 86 | sylan9eqr 2232 |
. . . . . . 7
      
                    |
88 | 80, 87 | eqtrd 2210 |
. . . . . 6
      
                    |
89 | 88 | ex 115 |
. . . . 5
 

   
         
          |
90 | 89 | expcom 116 |
. . . 4

      
                   |
91 | 90 | a2d 26 |
. . 3

      
         
           |
92 | 6, 11, 16, 21, 47, 91 | nn0ind 9343 |
. 2

            |
93 | 1, 92 | mpcom 36 |
1
           |