Step | Hyp | Ref
| Expression |
1 | | fveq2 5515 |
. . . . . 6
 mulGrp  mulGrp    |
2 | | isring.g |
. . . . . 6
mulGrp   |
3 | 1, 2 | eqtr4di 2228 |
. . . . 5
 mulGrp    |
4 | 3 | eleq1d 2246 |
. . . 4
  mulGrp 
   |
5 | | basfn 12514 |
. . . . . . 7
 |
6 | | vex 2740 |
. . . . . . 7
 |
7 | | funfvex 5532 |
. . . . . . . 8
 
       |
8 | 7 | funfni 5316 |
. . . . . . 7
 
       |
9 | 5, 6, 8 | mp2an 426 |
. . . . . 6
     |
10 | 9 | a1i 9 |
. . . . 5
       |
11 | | fveq2 5515 |
. . . . . 6
           |
12 | | isring.b |
. . . . . 6
     |
13 | 11, 12 | eqtr4di 2228 |
. . . . 5
       |
14 | | plusgslid 12565 |
. . . . . . . . 9
 Slot      
  |
15 | 14 | slotex 12483 |
. . . . . . . 8
      |
16 | 15 | elv 2741 |
. . . . . . 7
    |
17 | 16 | a1i 9 |
. . . . . 6
 
      |
18 | | simpl 109 |
. . . . . . . 8
 
   |
19 | 18 | fveq2d 5519 |
. . . . . . 7
 
         |
20 | | isring.p |
. . . . . . 7
    |
21 | 19, 20 | eqtr4di 2228 |
. . . . . 6
 
     |
22 | | mulrslid 12584 |
. . . . . . . . . 10
 Slot    
      |
23 | 22 | slotex 12483 |
. . . . . . . . 9
       |
24 | 23 | elv 2741 |
. . . . . . . 8
     |
25 | 24 | a1i 9 |
. . . . . . 7
          |
26 | | simpll 527 |
. . . . . . . . 9
      |
27 | 26 | fveq2d 5519 |
. . . . . . . 8
              |
28 | | isring.t |
. . . . . . . 8
     |
29 | 27, 28 | eqtr4di 2228 |
. . . . . . 7
         |
30 | | simpllr 534 |
. . . . . . . 8
       |
31 | | simpr 110 |
. . . . . . . . . . . . 13
      |
32 | | eqidd 2178 |
. . . . . . . . . . . . 13
       |
33 | | simplr 528 |
. . . . . . . . . . . . . 14
      |
34 | 33 | oveqd 5891 |
. . . . . . . . . . . . 13
             |
35 | 31, 32, 34 | oveq123d 5895 |
. . . . . . . . . . . 12
                   |
36 | 31 | oveqd 5891 |
. . . . . . . . . . . . 13
             |
37 | 31 | oveqd 5891 |
. . . . . . . . . . . . 13
             |
38 | 33, 36, 37 | oveq123d 5895 |
. . . . . . . . . . . 12
                    
    |
39 | 35, 38 | eqeq12d 2192 |
. . . . . . . . . . 11
                         
      
      |
40 | 33 | oveqd 5891 |
. . . . . . . . . . . . 13
             |
41 | | eqidd 2178 |
. . . . . . . . . . . . 13
       |
42 | 31, 40, 41 | oveq123d 5895 |
. . . . . . . . . . . 12
                   |
43 | 31 | oveqd 5891 |
. . . . . . . . . . . . 13
             |
44 | 33, 37, 43 | oveq123d 5895 |
. . . . . . . . . . . 12
                         |
45 | 42, 44 | eqeq12d 2192 |
. . . . . . . . . . 11
                         
 
    
      |
46 | 39, 45 | anbi12d 473 |
. . . . . . . . . 10
                                                        
 
 
    
       |
47 | 30, 46 | raleqbidv 2684 |
. . . . . . . . 9
      
                                                  
                 |
48 | 30, 47 | raleqbidv 2684 |
. . . . . . . 8
      

                                           
       
                 |
49 | 30, 48 | raleqbidv 2684 |
. . . . . . 7
      


                                           

       
                 |
50 | 25, 29, 49 | sbcied2 3000 |
. . . . . 6
           ![]. ].](_drbrack.gif) 


                                           

       
                 |
51 | 17, 21, 50 | sbcied2 3000 |
. . . . 5
 
       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)                                               

       
                 |
52 | 10, 13, 51 | sbcied2 3000 |
. . . 4
        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif) 


                                           

       
                 |
53 | 4, 52 | anbi12d 473 |
. . 3
   mulGrp        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif) 


                                          
 


 
      
 
 
    
        |
54 | | df-ring 13134 |
. . 3
  mulGrp        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif) 


                                             |
55 | 53, 54 | elrab2 2896 |
. 2


 


 
      
 
 
    
        |
56 | | 3anass 982 |
. 2
 



  
                    
 


 
      
 
 
    
        |
57 | 55, 56 | bitr4i 187 |
1


           
 
 
    
       |