Step | Hyp | Ref
| Expression |
1 | | eqid 2451 |
. . . 4
         |
2 | | eqid 2451 |
. . . 4
         |
3 | | keridl.1 |
. . . 4
     |
4 | | eqid 2451 |
. . . 4
 |
5 | 1, 2, 3, 4 | rngohomf 32205 |
. . 3
 

 
       
  |
6 | | cnvimass 5188 |
. . . 4
        |
7 | | fdm 5733 |
. . . 4
               |
8 | 6, 7 | syl5sseq 3480 |
. . 3
                      |
9 | 5, 8 | syl 17 |
. 2
 

 
      
      |
10 | | eqid 2451 |
. . . . 5
GId      GId       |
11 | 1, 2, 10 | rngo0cl 26126 |
. . . 4
 GId            |
12 | 11 | 3ad2ant1 1029 |
. . 3
 

 
GId            |
13 | | keridl.2 |
. . . . 5
GId   |
14 | 1, 10, 3, 13 | rngohom0 32211 |
. . . 4
 

 
   GId         |
15 | | fvex 5875 |
. . . . 5
   GId        |
16 | 15 | elsnc 3992 |
. . . 4
    GId        
   GId         |
17 | 14, 16 | sylibr 216 |
. . 3
 

 
   GId           |
18 | | ffn 5728 |
. . . 4
               |
19 | | elpreima 6002 |
. . . 4
      GId            
 GId             GId             |
20 | 5, 18, 19 | 3syl 18 |
. . 3
 

 
 GId            
 GId             GId             |
21 | 12, 17, 20 | mpbir2and 933 |
. 2
 

 
GId               |
22 | | an4 833 |
. . . . . . . 8
                          
     
           
          |
23 | 1, 2, 3 | rngohomadd 32208 |
. . . . . . . . . . . . . 14
  
                                        |
24 | 23 | adantr 467 |
. . . . . . . . . . . . 13
   
   
                                               |
25 | | oveq12 6299 |
. . . . . . . . . . . . . 14
                             |
26 | 25 | adantl 468 |
. . . . . . . . . . . . 13
   
   
                                       |
27 | 3 | rngogrpo 26118 |
. . . . . . . . . . . . . . . 16
   |
28 | 4, 13 | grpoidcl 25945 |
. . . . . . . . . . . . . . . . 17

  |
29 | 4, 13 | grpolid 25947 |
. . . . . . . . . . . . . . . . 17
         |
30 | 28, 29 | mpdan 674 |
. . . . . . . . . . . . . . . 16

      |
31 | 27, 30 | syl 17 |
. . . . . . . . . . . . . . 15
       |
32 | 31 | 3ad2ant2 1030 |
. . . . . . . . . . . . . 14
 

 
      |
33 | 32 | ad2antrr 732 |
. . . . . . . . . . . . 13
   
   
                           |
34 | 24, 26, 33 | 3eqtrd 2489 |
. . . . . . . . . . . 12
   
   
                                   |
35 | 34 | ex 436 |
. . . . . . . . . . 11
  
                                        |
36 | | fvex 5875 |
. . . . . . . . . . . . 13
     |
37 | 36 | elsnc 3992 |
. . . . . . . . . . . 12
             |
38 | | fvex 5875 |
. . . . . . . . . . . . 13
     |
39 | 38 | elsnc 3992 |
. . . . . . . . . . . 12
             |
40 | 37, 39 | anbi12i 703 |
. . . . . . . . . . 11
              
    
       |
41 | | fvex 5875 |
. . . . . . . . . . . 12
             |
42 | 41 | elsnc 3992 |
. . . . . . . . . . 11
                             |
43 | 35, 40, 42 | 3imtr4g 274 |
. . . . . . . . . 10
  
                            
                 |
44 | 43 | imdistanda 699 |
. . . . . . . . 9
 

 
                                
                       |
45 | 1, 2 | rngogcl 26119 |
. . . . . . . . . . . 12
     
                   |
46 | 45 | 3expib 1211 |
. . . . . . . . . . 11
                           |
47 | 46 | 3ad2ant1 1029 |
. . . . . . . . . 10
 

 
     
                    |
48 | 47 | anim1d 568 |
. . . . . . . . 9
 

 
                                       
                  |
49 | 44, 48 | syld 45 |
. . . . . . . 8
 

 
                                                          |
50 | 22, 49 | syl5bi 221 |
. . . . . . 7
 

 
                                                          |
51 | | elpreima 6002 |
. . . . . . . . 9
            
    
          |
52 | 5, 18, 51 | 3syl 18 |
. . . . . . . 8
 

 
       
    
          |
53 | | elpreima 6002 |
. . . . . . . . 9
            
    
          |
54 | 5, 18, 53 | 3syl 18 |
. . . . . . . 8
 

 
       
    
          |
55 | 52, 54 | anbi12d 717 |
. . . . . . 7
 

 
                      
                       |
56 | | elpreima 6002 |
. . . . . . . 8
                                                    |
57 | 5, 18, 56 | 3syl 18 |
. . . . . . 7
 

 
               
            
                  |
58 | 50, 55, 57 | 3imtr4d 272 |
. . . . . 6
 

 
                                   |
59 | 58 | impl 626 |
. . . . 5
   
  
                                 |
60 | 59 | ralrimiva 2802 |
. . . 4
  
                                     |
61 | 37 | anbi2i 700 |
. . . . . . 7
                 
       |
62 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
         |
63 | 1, 62, 2 | rngocl 26110 |
. . . . . . . . . . . . . . 15
     
                   |
64 | 63 | 3expb 1209 |
. . . . . . . . . . . . . 14
      
                    |
65 | 64 | 3ad2antl1 1170 |
. . . . . . . . . . . . 13
  
                            |
66 | 65 | anass1rs 816 |
. . . . . . . . . . . 12
   
  
    
                   |
67 | 66 | adantlrr 727 |
. . . . . . . . . . 11
   
   
                             |
68 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
         |
69 | 1, 2, 62, 68 | rngohommul 32209 |
. . . . . . . . . . . . . . 15
  
                                            |
70 | 69 | anass1rs 816 |
. . . . . . . . . . . . . 14
   
  
    
                                   |
71 | 70 | adantlrr 727 |
. . . . . . . . . . . . 13
   
   
                                             |
72 | | oveq2 6298 |
. . . . . . . . . . . . . . 15
                                   |
73 | 72 | adantl 468 |
. . . . . . . . . . . . . 14
                                         |
74 | 73 | ad2antlr 733 |
. . . . . . . . . . . . 13
   
   
                                             |
75 | 1, 2, 3, 4 | rngohomcl 32206 |
. . . . . . . . . . . . . . 15
  
              |
76 | 13, 4, 3, 68 | rngorz 26130 |
. . . . . . . . . . . . . . . 16
                     |
77 | 76 | 3ad2antl2 1171 |
. . . . . . . . . . . . . . 15
  
                      |
78 | 75, 77 | syldan 473 |
. . . . . . . . . . . . . 14
  
                      |
79 | 78 | adantlr 721 |
. . . . . . . . . . . . 13
   
   
                             |
80 | 71, 74, 79 | 3eqtrd 2489 |
. . . . . . . . . . . 12
   
   
                             |
81 | | fvex 5875 |
. . . . . . . . . . . . 13
             |
82 | 81 | elsnc 3992 |
. . . . . . . . . . . 12
                             |
83 | 80, 82 | sylibr 216 |
. . . . . . . . . . 11
   
   
                               |
84 | | elpreima 6002 |
. . . . . . . . . . . . 13
                                                    |
85 | 5, 18, 84 | 3syl 18 |
. . . . . . . . . . . 12
 

 
               
            
                  |
86 | 85 | ad2antrr 732 |
. . . . . . . . . . 11
   
   
                                                              |
87 | 67, 83, 86 | mpbir2and 933 |
. . . . . . . . . 10
   
   
                                |
88 | 1, 62, 2 | rngocl 26110 |
. . . . . . . . . . . . . . 15
     
                   |
89 | 88 | 3expb 1209 |
. . . . . . . . . . . . . 14
      
                    |
90 | 89 | 3ad2antl1 1170 |
. . . . . . . . . . . . 13
  
                            |
91 | 90 | anassrs 654 |
. . . . . . . . . . . 12
   
  
    
                   |
92 | 91 | adantlrr 727 |
. . . . . . . . . . 11
   
   
                             |
93 | 1, 2, 62, 68 | rngohommul 32209 |
. . . . . . . . . . . . . . 15
  
                                            |
94 | 93 | anassrs 654 |
. . . . . . . . . . . . . 14
   
  
    
                                   |
95 | 94 | adantlrr 727 |
. . . . . . . . . . . . 13
   
   
                                             |
96 | | oveq1 6297 |
. . . . . . . . . . . . . . 15
                                   |
97 | 96 | adantl 468 |
. . . . . . . . . . . . . 14
                                         |
98 | 97 | ad2antlr 733 |
. . . . . . . . . . . . 13
   
   
                                             |
99 | 13, 4, 3, 68 | rngolz 26129 |
. . . . . . . . . . . . . . . 16
                     |
100 | 99 | 3ad2antl2 1171 |
. . . . . . . . . . . . . . 15
  
                      |
101 | 75, 100 | syldan 473 |
. . . . . . . . . . . . . 14
  
                      |
102 | 101 | adantlr 721 |
. . . . . . . . . . . . 13
   
   
                             |
103 | 95, 98, 102 | 3eqtrd 2489 |
. . . . . . . . . . . 12
   
   
                             |
104 | | fvex 5875 |
. . . . . . . . . . . . 13
             |
105 | 104 | elsnc 3992 |
. . . . . . . . . . . 12
                             |
106 | 103, 105 | sylibr 216 |
. . . . . . . . . . 11
   
   
                               |
107 | | elpreima 6002 |
. . . . . . . . . . . . 13
                                                    |
108 | 5, 18, 107 | 3syl 18 |
. . . . . . . . . . . 12
 

 
               
            
                  |
109 | 108 | ad2antrr 732 |
. . . . . . . . . . 11
   
   
                                                              |
110 | 92, 106, 109 | mpbir2and 933 |
. . . . . . . . . 10
   
   
                                |
111 | 87, 110 | jca 535 |
. . . . . . . . 9
   
   
                                                 |
112 | 111 | ralrimiva 2802 |
. . . . . . . 8
  
              
                                       |
113 | 112 | ex 436 |
. . . . . . 7
 

 
           
                                        |
114 | 61, 113 | syl5bi 221 |
. . . . . 6
 

 
            
                                         |
115 | 52, 114 | sylbid 219 |
. . . . 5
 

 
        
                                        |
116 | 115 | imp 431 |
. . . 4
  
                                                   |
117 | 60, 116 | jca 535 |
. . 3
  
                                                                             |
118 | 117 | ralrimiva 2802 |
. 2
 

 
                                                                           |
119 | 1, 62, 2, 10 | isidl 32247 |
. . 3
                    
    GId             
                                                                            |
120 | 119 | 3ad2ant1 1029 |
. 2
 

 
                   
    GId             
                                                                            |
121 | 9, 21, 118, 120 | mpbir3and 1191 |
1
 

 
             |