Proof of Theorem rngcinv
Step | Hyp | Ref
| Expression |
1 | | rngcsect.b |
. . 3
     |
2 | | rngcinv.n |
. . 3
Inv   |
3 | | rngcsect.u |
. . . 4
   |
4 | | rngcsect.c |
. . . . 5
RngCat   |
5 | 4 | rngccat 40033 |
. . . 4
   |
6 | 3, 5 | syl 17 |
. . 3
   |
7 | | rngcsect.x |
. . 3
   |
8 | | rngcsect.y |
. . 3
   |
9 | | eqid 2451 |
. . 3
Sect  Sect   |
10 | 1, 2, 6, 7, 8, 9 | isinv 15665 |
. 2
            Sect        Sect         |
11 | | eqid 2451 |
. . . . . 6
         |
12 | 4, 1, 3, 7, 8, 11,
9 | rngcsect 40035 |
. . . . 5
     Sect    
  RngHomo

 RngHomo  

         |
13 | | df-3an 987 |
. . . . 5
   RngHomo   RngHomo
        
 
 RngHomo   RngHomo
 
 
        |
14 | 12, 13 | syl6bb 265 |
. . . 4
     Sect    
 
 RngHomo   RngHomo
 
 
         |
15 | | eqid 2451 |
. . . . . 6
         |
16 | 4, 1, 3, 8, 7, 15,
9 | rngcsect 40035 |
. . . . 5
     Sect    
  RngHomo

 RngHomo  

         |
17 | | 3ancoma 992 |
. . . . . 6
   RngHomo   RngHomo
        
  RngHomo

 RngHomo  

        |
18 | | df-3an 987 |
. . . . . 6
   RngHomo   RngHomo
        
 
 RngHomo   RngHomo
 
 
        |
19 | 17, 18 | bitri 253 |
. . . . 5
   RngHomo   RngHomo
        
 
 RngHomo   RngHomo
 
 
        |
20 | 16, 19 | syl6bb 265 |
. . . 4
     Sect    
 
 RngHomo   RngHomo
 
 
         |
21 | 14, 20 | anbi12d 717 |
. . 3
      Sect        Sect          RngHomo 

RngHomo    
         RngHomo 

RngHomo    
          |
22 | | anandi 837 |
. . 3
     RngHomo

 RngHomo   
          RngHomo

 RngHomo   
             RngHomo   RngHomo
 
 
        RngHomo

 RngHomo        RngHomo   RngHomo
 
 
       
         |
23 | 21, 22 | syl6bb 265 |
. 2
      Sect        Sect           RngHomo   RngHomo
 
 
        RngHomo

 RngHomo        RngHomo   RngHomo
 
 
       
          |
24 | | simplrl 770 |
. . . . . 6
      RngHomo 

RngHomo    
        RngHomo

 RngHomo        RngHomo   RngHomo
 
 
       
      

RngHomo    |
25 | 24 | adantl 468 |
. . . . 5
 
     RngHomo

 RngHomo   
       
 RngHomo   RngHomo
       RngHomo

 RngHomo   
       
        

RngHomo    |
26 | 11, 15 | rnghmf 39952 |
. . . . . . . . . 10
  RngHomo 
              |
27 | 15, 11 | rnghmf 39952 |
. . . . . . . . . 10
  RngHomo 
              |
28 | 26, 27 | anim12i 570 |
. . . . . . . . 9
   RngHomo   RngHomo
 
            
               |
29 | 28 | ad2antlr 733 |
. . . . . . . 8
      RngHomo 

RngHomo    
        RngHomo

 RngHomo        RngHomo   RngHomo
 
 
       
      
            
               |
30 | | simpr 463 |
. . . . . . . . 9
     RngHomo

 RngHomo   
       
                |
31 | 30 | adantl 468 |
. . . . . . . 8
      RngHomo 

RngHomo    
        RngHomo

 RngHomo        RngHomo   RngHomo
 
 
       
      
 
       |
32 | | simpr 463 |
. . . . . . . . 9
    RngHomo   RngHomo
 
 
       
       |
33 | 32 | ad2antrl 734 |
. . . . . . . 8
      RngHomo 

RngHomo    
        RngHomo

 RngHomo        RngHomo   RngHomo
 
 
       
      
 
       |
34 | 29, 31, 33 | jca32 538 |
. . . . . . 7
      RngHomo 

RngHomo    
        RngHomo

 RngHomo        RngHomo   RngHomo
 
 
       
      
             
            
 

      
         |
35 | 34 | adantl 468 |
. . . . . 6
 
     RngHomo

 RngHomo   
       
 RngHomo   RngHomo
       RngHomo

 RngHomo   
       
        
             
            
 

      
         |
36 | | fcof1o 6194 |
. . . . . . 7
                              
     
                     
   |
37 | | eqcom 2458 |
. . . . . . . 8
 
   |
38 | 37 | anbi2i 700 |
. . . . . . 7
             
 
            
    |
39 | 36, 38 | sylib 200 |
. . . . . 6
                              
     
                    
    |
40 | 35, 39 | syl 17 |
. . . . 5
 
     RngHomo

 RngHomo   
       
 RngHomo   RngHomo
       RngHomo

 RngHomo   
       
        
            
    |
41 | | anass 655 |
. . . . 5
    RngHomo              
 
  RngHomo
             
     |
42 | 25, 40, 41 | sylanbrc 670 |
. . . 4
 
     RngHomo

 RngHomo   
       
 RngHomo   RngHomo
       RngHomo

 RngHomo   
       
        
 
 RngHomo                   |
43 | 11, 15 | isrngim 39957 |
. . . . . . 7
 
   RngIsom 
  RngHomo
                 |
44 | 7, 8, 43 | syl2anc 667 |
. . . . . 6
   RngIsom 
  RngHomo
                 |
45 | 44 | anbi1d 711 |
. . . . 5
    RngIsom

 
 
 RngHomo                    |
46 | 45 | adantr 467 |
. . . 4
 
     RngHomo

 RngHomo   
       
 RngHomo   RngHomo
       RngHomo

 RngHomo   
       
        
 
 RngIsom   
 
 RngHomo                    |
47 | 42, 46 | mpbird 236 |
. . 3
 
     RngHomo

 RngHomo   
       
 RngHomo   RngHomo
       RngHomo

 RngHomo   
       
        
  RngIsom

    |
48 | 11, 15 | rngimrnghm 39959 |
. . . . . 6
  RngIsom 

RngHomo    |
49 | 48 | ad2antrl 734 |
. . . . 5
 
  RngIsom

  
 RngHomo    |
50 | | isrngisom 39949 |
. . . . . . . . . . 11
 
   RngIsom 
  RngHomo
 
 RngHomo      |
51 | 7, 8, 50 | syl2anc 667 |
. . . . . . . . . 10
   RngIsom 
  RngHomo
 
 RngHomo      |
52 | | eleq1 2517 |
. . . . . . . . . . . 12
     RngHomo
  RngHomo     |
53 | 52 | eqcoms 2459 |
. . . . . . . . . . 11
     RngHomo
  RngHomo     |
54 | 53 | anbi2d 710 |
. . . . . . . . . 10
     RngHomo
 
 RngHomo  
  RngHomo

 RngHomo      |
55 | 51, 54 | sylan9bbr 707 |
. . . . . . . . 9
    
 RngIsom    RngHomo

 RngHomo      |
56 | | simpr 463 |
. . . . . . . . 9
   RngHomo   RngHomo
 

RngHomo    |
57 | 55, 56 | syl6bi 232 |
. . . . . . . 8
    
 RngIsom 

RngHomo     |
58 | 57 | com12 32 |
. . . . . . 7
  RngIsom 
 
   RngHomo
    |
59 | 58 | expdimp 439 |
. . . . . 6
   RngIsom      RngHomo     |
60 | 59 | impcom 432 |
. . . . 5
 
  RngIsom

  
 RngHomo    |
61 | | coeq1 4992 |
. . . . . . 7
         |
62 | 61 | ad2antll 735 |
. . . . . 6
 
  RngIsom

          |
63 | 11, 15 | rngimf1o 39958 |
. . . . . . . 8
  RngIsom 
              |
64 | 63 | ad2antrl 734 |
. . . . . . 7
 
  RngIsom

                 |
65 | | f1ococnv1 5842 |
. . . . . . 7
               
       |
66 | 64, 65 | syl 17 |
. . . . . 6
 
  RngIsom

     
       |
67 | 62, 66 | eqtrd 2485 |
. . . . 5
 
  RngIsom

            |
68 | 49, 60, 67 | jca31 537 |
. . . 4
 
  RngIsom

      RngHomo

 RngHomo   
         |
69 | 51 | biimpcd 228 |
. . . . . . 7
  RngIsom 
   RngHomo  
 RngHomo      |
70 | 69 | adantr 467 |
. . . . . 6
   RngIsom       RngHomo
 
 RngHomo      |
71 | 70 | impcom 432 |
. . . . 5
 
  RngIsom

     RngHomo  
 RngHomo     |
72 | | eleq1 2517 |
. . . . . . 7
    RngHomo 
  RngHomo
    |
73 | 72 | ad2antll 735 |
. . . . . 6
 
  RngIsom

     RngHomo 
  RngHomo
    |
74 | 73 | anbi2d 710 |
. . . . 5
 
  RngIsom

      RngHomo

 RngHomo  
  RngHomo
 
 RngHomo      |
75 | 71, 74 | mpbird 236 |
. . . 4
 
  RngIsom

     RngHomo   RngHomo
    |
76 | | coeq2 4993 |
. . . . . . 7
         |
77 | 76 | ad2antll 735 |
. . . . . 6
 
  RngIsom

          |
78 | | f1ococnv2 5840 |
. . . . . . 7
               
       |
79 | 64, 78 | syl 17 |
. . . . . 6
 
  RngIsom

     
       |
80 | 77, 79 | eqtrd 2485 |
. . . . 5
 
  RngIsom

            |
81 | 75, 67, 80 | jca31 537 |
. . . 4
 
  RngIsom

       RngHomo 

RngHomo    
       
        |
82 | 68, 75, 81 | jca31 537 |
. . 3
 
  RngIsom

        RngHomo   RngHomo
 
 
        RngHomo

 RngHomo        RngHomo   RngHomo
 
 
       
         |
83 | 47, 82 | impbida 843 |
. 2
       RngHomo   RngHomo
 
 
        RngHomo

 RngHomo        RngHomo   RngHomo
 
 
       
         RngIsom

     |
84 | 10, 23, 83 | 3bitrd 283 |
1
          RngIsom       |