Step | Hyp | Ref
| Expression |
1 | | grpkerinj.2 |
. . . . . . . . 9
GId   |
2 | | grpkerinj.4 |
. . . . . . . . 9
GId   |
3 | 1, 2 | ghomidOLD 26086 |
. . . . . . . 8
 

GrpOpHom         |
4 | 3 | sneqd 3979 |
. . . . . . 7
 

GrpOpHom             |
5 | | grpkerinj.1 |
. . . . . . . . . 10
 |
6 | | grpkerinj.3 |
. . . . . . . . . 10
 |
7 | 5, 6 | ghomf 32173 |
. . . . . . . . 9
 

GrpOpHom         |
8 | | ffn 5726 |
. . . . . . . . 9
    
  |
9 | 7, 8 | syl 17 |
. . . . . . . 8
 

GrpOpHom     |
10 | 5, 1 | grpoidcl 25938 |
. . . . . . . . 9

  |
11 | 10 | 3ad2ant1 1028 |
. . . . . . . 8
 

GrpOpHom     |
12 | | fnsnfv 5923 |
. . . . . . . 8
 
               |
13 | 9, 11, 12 | syl2anc 666 |
. . . . . . 7
 

GrpOpHom                 |
14 | 4, 13 | eqtr3d 2486 |
. . . . . 6
 

GrpOpHom             |
15 | 14 | imaeq2d 5167 |
. . . . 5
 

GrpOpHom                       |
16 | 15 | adantl 468 |
. . . 4
        GrpOpHom
                       |
17 | 10 | snssd 4116 |
. . . . . 6

    |
18 | 17 | 3ad2ant1 1028 |
. . . . 5
 

GrpOpHom       |
19 | | f1imacnv 5828 |
. . . . 5
                        |
20 | 18, 19 | sylan2 477 |
. . . 4
        GrpOpHom
                  |
21 | 16, 20 | eqtrd 2484 |
. . 3
        GrpOpHom
              |
22 | 21 | expcom 437 |
. 2
 

GrpOpHom       
            |
23 | 7 | adantr 467 |
. . . 4
    GrpOpHom
 
                |
24 | | simpl2 1011 |
. . . . . . . 8
    GrpOpHom
 

 
  |
25 | 7 | ffvelrnda 6020 |
. . . . . . . . 9
    GrpOpHom
 
       |
26 | 25 | adantrr 722 |
. . . . . . . 8
    GrpOpHom
 

        |
27 | 7 | ffvelrnda 6020 |
. . . . . . . . 9
    GrpOpHom
 
       |
28 | 27 | adantrl 721 |
. . . . . . . 8
    GrpOpHom
 

        |
29 | | eqid 2450 |
. . . . . . . . 9
     |
30 | 6, 2, 29 | grpoeqdivid 32172 |
. . . . . . . 8
     
             
     
           |
31 | 24, 26, 28, 30 | syl3anc 1267 |
. . . . . . 7
    GrpOpHom
 

                            |
32 | 31 | adantlr 720 |
. . . . . 6
     GrpOpHom             
 
        
     
           |
33 | | eqid 2450 |
. . . . . . . . . 10
     |
34 | 5, 33, 29 | ghomdiv 32175 |
. . . . . . . . 9
    GrpOpHom
 

                            |
35 | 34 | adantlr 720 |
. . . . . . . 8
     GrpOpHom             
 
                          |
36 | 35 | eqeq1d 2452 |
. . . . . . 7
     GrpOpHom             
 
     
                      |
37 | | fvex 5873 |
. . . . . . . . . . 11
GId   |
38 | 2, 37 | eqeltri 2524 |
. . . . . . . . . 10
 |
39 | 38 | snid 3995 |
. . . . . . . . 9
   |
40 | | eleq1 2516 |
. . . . . . . . 9
                             |
41 | 39, 40 | mpbiri 237 |
. . . . . . . 8
               
         |
42 | | ffun 5729 |
. . . . . . . . . . . . . 14
       |
43 | 7, 42 | syl 17 |
. . . . . . . . . . . . 13
 

GrpOpHom  
  |
44 | 43 | adantr 467 |
. . . . . . . . . . . 12
    GrpOpHom
 

    |
45 | 5, 33 | grpodivcl 25968 |
. . . . . . . . . . . . . . 15
 
         |
46 | 45 | 3expb 1208 |
. . . . . . . . . . . . . 14
  
 
 
      |
47 | 46 | 3ad2antl1 1169 |
. . . . . . . . . . . . 13
    GrpOpHom
 

          |
48 | | fdm 5731 |
. . . . . . . . . . . . . . 15
       |
49 | 7, 48 | syl 17 |
. . . . . . . . . . . . . 14
 

GrpOpHom  
  |
50 | 49 | adantr 467 |
. . . . . . . . . . . . 13
    GrpOpHom
 

    |
51 | 47, 50 | eleqtrrd 2531 |
. . . . . . . . . . . 12
    GrpOpHom
 

          |
52 | | fvimacnv 5995 |
. . . . . . . . . . . 12
                                      |
53 | 44, 51, 52 | syl2anc 666 |
. . . . . . . . . . 11
    GrpOpHom
 

                               |
54 | | eleq2 2517 |
. . . . . . . . . . 11
         
             
 
         |
55 | 53, 54 | sylan9bb 705 |
. . . . . . . . . 10
     GrpOpHom   
                                    |
56 | 55 | an32s 812 |
. . . . . . . . 9
     GrpOpHom             
 
     
      
 
         |
57 | | elsni 3992 |
. . . . . . . . . . 11
                 |
58 | 5, 1, 33 | grpoeqdivid 32172 |
. . . . . . . . . . . . . 14
 
 
 
       |
59 | 58 | biimprd 227 |
. . . . . . . . . . . . 13
 
           |
60 | 59 | 3expb 1208 |
. . . . . . . . . . . 12
  
 
      
   |
61 | 60 | 3ad2antl1 1169 |
. . . . . . . . . . 11
    GrpOpHom
 

            |
62 | 57, 61 | syl5 33 |
. . . . . . . . . 10
    GrpOpHom
 

          
   |
63 | 62 | adantlr 720 |
. . . . . . . . 9
     GrpOpHom             
 
            |
64 | 56, 63 | sylbid 219 |
. . . . . . . 8
     GrpOpHom             
 
     
          |
65 | 41, 64 | syl5 33 |
. . . . . . 7
     GrpOpHom             
 
     
    
   |
66 | 36, 65 | sylbird 239 |
. . . . . 6
     GrpOpHom             
 
              
   |
67 | 32, 66 | sylbid 219 |
. . . . 5
     GrpOpHom             
 
            |
68 | 67 | ralrimivva 2808 |
. . . 4
    GrpOpHom
 
          

            |
69 | | dff13 6157 |
. . . 4
    
     

        
    |
70 | 23, 68, 69 | sylanbrc 669 |
. . 3
    GrpOpHom
 
                |
71 | 70 | ex 436 |
. 2
 

GrpOpHom            
       |
72 | 22, 71 | impbid 194 |
1
 

GrpOpHom       
            |