Step | Hyp | Ref
| Expression |
1 | | grpfo.1 |
. . . 4
 |
2 | 1 | grpoidinv 25936 |
. . 3



                         |
3 | | simpll 760 |
. . . . . . . . 9
            
                 |
4 | 3 | ralimi 2781 |
. . . . . . . 8
 
           
                  |
5 | | oveq2 6298 |
. . . . . . . . . 10
           |
6 | | id 22 |
. . . . . . . . . 10
   |
7 | 5, 6 | eqeq12d 2466 |
. . . . . . . . 9
     
       |
8 | 7 | cbvralv 3019 |
. . . . . . . 8
 
   

      |
9 | 4, 8 | sylib 200 |
. . . . . . 7
 
           
                  |
10 | 9 | adantl 468 |
. . . . . 6
                             
      |
11 | 9 | ad2antlr 733 |
. . . . . . . 8
    

                        

      |
12 | | simpr 463 |
. . . . . . . . . . . . . . . 16
            
                        |
13 | 12 | ralimi 2781 |
. . . . . . . . . . . . . . 15
 
           
            
            |
14 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . . 20
           |
15 | 14 | eqeq1d 2453 |
. . . . . . . . . . . . . . . . . . 19
     
       |
16 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . 20
           |
17 | 16 | eqeq1d 2453 |
. . . . . . . . . . . . . . . . . . 19
     
       |
18 | 15, 17 | anbi12d 717 |
. . . . . . . . . . . . . . . . . 18
                         |
19 | 18 | rexbidv 2901 |
. . . . . . . . . . . . . . . . 17
  
                        |
20 | 19 | rspcva 3148 |
. . . . . . . . . . . . . . . 16
   
          

            |
21 | 20 | adantll 720 |
. . . . . . . . . . . . . . 15
                 
            |
22 | 13, 21 | sylan2 477 |
. . . . . . . . . . . . . 14
                             
            |
23 | 1 | grpoidinvlem4 25935 |
. . . . . . . . . . . . . 14
                          |
24 | 22, 23 | syldan 473 |
. . . . . . . . . . . . 13
                                       |
25 | 24 | an32s 813 |
. . . . . . . . . . . 12
               
                       |
26 | 25 | adantllr 725 |
. . . . . . . . . . 11
    

                        
          |
27 | 26 | adantr 467 |
. . . . . . . . . 10
    
 
           
              
                     |
28 | | oveq2 6298 |
. . . . . . . . . . . . . . 15
           |
29 | | id 22 |
. . . . . . . . . . . . . . 15
   |
30 | 28, 29 | eqeq12d 2466 |
. . . . . . . . . . . . . 14
     
       |
31 | 30 | rspcva 3148 |
. . . . . . . . . . . . 13
              |
32 | 31 | adantll 720 |
. . . . . . . . . . . 12
         
      |
33 | 32 | ad2ant2rl 755 |
. . . . . . . . . . 11
    
  
                 |
34 | 33 | adantllr 725 |
. . . . . . . . . 10
    
 
           
              
                 |
35 | | oveq2 6298 |
. . . . . . . . . . . . 13
           |
36 | | id 22 |
. . . . . . . . . . . . 13
   |
37 | 35, 36 | eqeq12d 2466 |
. . . . . . . . . . . 12
     
       |
38 | 37 | rspcva 3148 |
. . . . . . . . . . 11
              |
39 | 38 | ad2ant2lr 754 |
. . . . . . . . . 10
    
 
           
              
                 |
40 | 27, 34, 39 | 3eqtr3d 2493 |
. . . . . . . . 9
    
 
           
              
             |
41 | 40 | ex 436 |
. . . . . . . 8
    

                        
  
         
   |
42 | 11, 41 | mpand 681 |
. . . . . . 7
    

                        
 
       |
43 | 42 | ralrimiva 2802 |
. . . . . 6
                             
 
       |
44 | 10, 43 | jca 535 |
. . . . 5
                              
          
    |
45 | 44 | ex 436 |
. . . 4
    
           
          
 
    
 
   
     |
46 | 45 | reximdva 2862 |
. . 3

 

           
                        
     |
47 | 2, 46 | mpd 15 |
. 2


 
    
 
   
    |
48 | | oveq1 6297 |
. . . . 5
           |
49 | 48 | eqeq1d 2453 |
. . . 4
     
       |
50 | 49 | ralbidv 2827 |
. . 3
  
   

       |
51 | 50 | reu8 3234 |
. 2
  
   

 
    
 
   
    |
52 | 47, 51 | sylibr 216 |
1



      |