Step | Hyp | Ref
| Expression |
1 | | elex 2749 |
. 2
 SRing   |
2 | | simp1 997 |
. . 3
  CMnd 
 

  
                     
 
CMnd |
3 | 2 | elexd 2751 |
. 2
  CMnd 
 

  
                     
 
  |
4 | | issrg.g |
. . . . . . . 8
mulGrp   |
5 | 4 | eleq1i 2243 |
. . . . . . 7

mulGrp    |
6 | 5 | bicomi 132 |
. . . . . 6
 mulGrp    |
7 | 6 | a1i 9 |
. . . . 5
  mulGrp 
   |
8 | | issrg.b |
. . . . . . 7
     |
9 | | basfn 12520 |
. . . . . . . 8
 |
10 | | funfvex 5533 |
. . . . . . . . 9
 
       |
11 | 10 | funfni 5317 |
. . . . . . . 8
 
       |
12 | 9, 11 | mpan 424 |
. . . . . . 7
       |
13 | 8, 12 | eqeltrid 2264 |
. . . . . 6
   |
14 | | issrg.p |
. . . . . . . . 9
    |
15 | | plusgslid 12571 |
. . . . . . . . . 10
 Slot      
  |
16 | 15 | slotex 12489 |
. . . . . . . . 9
      |
17 | 14, 16 | eqeltrid 2264 |
. . . . . . . 8
   |
18 | 17 | adantr 276 |
. . . . . . 7
 
   |
19 | | issrg.t |
. . . . . . . . . 10
     |
20 | | mulrslid 12590 |
. . . . . . . . . . 11
 Slot    
      |
21 | 20 | slotex 12489 |
. . . . . . . . . 10
       |
22 | 19, 21 | eqeltrid 2264 |
. . . . . . . . 9
   |
23 | 22 | ad2antrr 488 |
. . . . . . . 8
   
  |
24 | | issrg.0 |
. . . . . . . . . . 11
     |
25 | | fn0g 12794 |
. . . . . . . . . . . 12
 |
26 | | funfvex 5533 |
. . . . . . . . . . . . 13
         |
27 | 26 | funfni 5317 |
. . . . . . . . . . . 12
 
       |
28 | 25, 27 | mpan 424 |
. . . . . . . . . . 11
       |
29 | 24, 28 | eqeltrid 2264 |
. . . . . . . . . 10
   |
30 | 29 | ad3antrrr 492 |
. . . . . . . . 9
   
   |
31 | | simp-4r 542 |
. . . . . . . . . 10
        |
32 | | simplr 528 |
. . . . . . . . . . . . . . . 16
       |
33 | | eqidd 2178 |
. . . . . . . . . . . . . . . 16
        |
34 | | simpllr 534 |
. . . . . . . . . . . . . . . . 17
       |
35 | 34 | oveqd 5892 |
. . . . . . . . . . . . . . . 16
              |
36 | 32, 33, 35 | oveq123d 5896 |
. . . . . . . . . . . . . . 15
                    |
37 | 32 | oveqd 5892 |
. . . . . . . . . . . . . . . 16
              |
38 | 32 | oveqd 5892 |
. . . . . . . . . . . . . . . 16
              |
39 | 34, 37, 38 | oveq123d 5896 |
. . . . . . . . . . . . . . 15
                     
    |
40 | 36, 39 | eqeq12d 2192 |
. . . . . . . . . . . . . 14
                          
      
      |
41 | 34 | oveqd 5892 |
. . . . . . . . . . . . . . . 16
              |
42 | | eqidd 2178 |
. . . . . . . . . . . . . . . 16
        |
43 | 32, 41, 42 | oveq123d 5896 |
. . . . . . . . . . . . . . 15
                    |
44 | 32 | oveqd 5892 |
. . . . . . . . . . . . . . . 16
              |
45 | 34, 38, 44 | oveq123d 5896 |
. . . . . . . . . . . . . . 15
                          |
46 | 43, 45 | eqeq12d 2192 |
. . . . . . . . . . . . . 14
                          
 
    
      |
47 | 40, 46 | anbi12d 473 |
. . . . . . . . . . . . 13
                                                         
 
 
    
       |
48 | 31, 47 | raleqbidv 2685 |
. . . . . . . . . . . 12
       
                                                  
                 |
49 | 31, 48 | raleqbidv 2685 |
. . . . . . . . . . 11
       

                                           
       
                 |
50 | | simpr 110 |
. . . . . . . . . . . . . 14
       |
51 | 32, 50, 33 | oveq123d 5896 |
. . . . . . . . . . . . 13
             |
52 | 51, 50 | eqeq12d 2192 |
. . . . . . . . . . . 12
          
   |
53 | 32, 33, 50 | oveq123d 5896 |
. . . . . . . . . . . . 13
             |
54 | 53, 50 | eqeq12d 2192 |
. . . . . . . . . . . 12
          
   |
55 | 52, 54 | anbi12d 473 |
. . . . . . . . . . 11
                   
   |
56 | 49, 55 | anbi12d 473 |
. . . . . . . . . 10
                                                                

 
      
 
 
    
      
    |
57 | 31, 56 | raleqbidv 2685 |
. . . . . . . . 9
       
                                                           
       
                
    |
58 | 30, 57 | sbcied 3000 |
. . . . . . . 8
   
   ![]. ].](_drbrack.gif) 
                                                           
       
                
    |
59 | 23, 58 | sbcied 3000 |
. . . . . . 7
      ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif)                                                             
       
                
    |
60 | 18, 59 | sbcied 3000 |
. . . . . 6
 
   ![]. ].](_drbrack.gif)
 ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif)                                                             
       
                
    |
61 | 13, 60 | sbcied 3000 |
. . . . 5
  
 ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif)
 ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif)                                                             
       
                
    |
62 | 7, 61 | anbi12d 473 |
. . . 4
   mulGrp    ![]. ].](_drbrack.gif)
 ![]. ].](_drbrack.gif)
 ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif) 
                                                        
 
 

  
                     
     |
63 | 62 | anbi2d 464 |
. . 3
   CMnd  mulGrp    ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif)
 ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif)                                                           
 CMnd 

 

  
                     
      |
64 | | fveq2 5516 |
. . . . . 6
 mulGrp  mulGrp    |
65 | 64 | eleq1d 2246 |
. . . . 5
  mulGrp  mulGrp     |
66 | | fveq2 5516 |
. . . . . . 7
           |
67 | 66, 8 | eqtr4di 2228 |
. . . . . 6
       |
68 | | fveq2 5516 |
. . . . . . . 8
         |
69 | 68, 14 | eqtr4di 2228 |
. . . . . . 7
     |
70 | | fveq2 5516 |
. . . . . . . . 9
           |
71 | 70, 19 | eqtr4di 2228 |
. . . . . . . 8
      |
72 | | fveq2 5516 |
. . . . . . . . . 10
           |
73 | 72, 24 | eqtr4di 2228 |
. . . . . . . . 9
      |
74 | 73 | sbceq1d 2968 |
. . . . . . . 8
        ![]. ].](_drbrack.gif) 
                                                         ![]. ].](_drbrack.gif)                                                             |
75 | 71, 74 | sbceqbid 2970 |
. . . . . . 7
        ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif) 
                                                       
 ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif)                                                             |
76 | 69, 75 | sbceqbid 2970 |
. . . . . 6
       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif) 
                                                         ![]. ].](_drbrack.gif)
 ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif)                                                             |
77 | 67, 76 | sbceqbid 2970 |
. . . . 5
        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif) 
                                                          ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif)
 ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif)                                                             |
78 | 65, 77 | anbi12d 473 |
. . . 4
   mulGrp        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif) 
                                                        
 mulGrp    ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif)
 ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif)                                                              |
79 | | df-srg 13147 |
. . . 4
SRing  CMnd
 mulGrp        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)                                                             |
80 | 78, 79 | elrab2 2897 |
. . 3
 SRing  CMnd  mulGrp    ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif)
 ![]. ].](_drbrack.gif)  ![]. ].](_drbrack.gif)                                                              |
81 | | 3anass 982 |
. . 3
  CMnd 
 

  
                     
 
 CMnd 

 

  
                     
     |
82 | 63, 80, 81 | 3bitr4g 223 |
. 2
 
SRing  CMnd
   
       
                
     |
83 | 1, 3, 82 | pm5.21nii 704 |
1
 SRing  CMnd

 

       
                
    |