Proof of Theorem ringcinv
Step | Hyp | Ref
| Expression |
1 | | ringcsect.b |
. . 3
     |
2 | | ringcinv.n |
. . 3
Inv   |
3 | | ringcsect.u |
. . . 4
   |
4 | | ringcsect.c |
. . . . 5
RingCat   |
5 | 4 | ringccat 40013 |
. . . 4
   |
6 | 3, 5 | syl 17 |
. . 3
   |
7 | | ringcsect.x |
. . 3
   |
8 | | ringcsect.y |
. . 3
   |
9 | | eqid 2450 |
. . 3
Sect  Sect   |
10 | 1, 2, 6, 7, 8, 9 | isinv 15658 |
. 2
            Sect        Sect         |
11 | | eqid 2450 |
. . . . . 6
         |
12 | 4, 1, 3, 7, 8, 11,
9 | ringcsect 40020 |
. . . . 5
     Sect    
  RingHom

 RingHom  

         |
13 | | df-3an 986 |
. . . . 5
   RingHom   RingHom
        
 
 RingHom   RingHom
 
 
        |
14 | 12, 13 | syl6bb 265 |
. . . 4
     Sect    
 
 RingHom   RingHom
 
 
         |
15 | | eqid 2450 |
. . . . . 6
         |
16 | 4, 1, 3, 8, 7, 15,
9 | ringcsect 40020 |
. . . . 5
     Sect    
  RingHom

 RingHom  

         |
17 | | 3ancoma 991 |
. . . . . 6
   RingHom   RingHom
        
  RingHom

 RingHom  

        |
18 | | df-3an 986 |
. . . . . 6
   RingHom   RingHom
        
 
 RingHom   RingHom
 
 
        |
19 | 17, 18 | bitri 253 |
. . . . 5
   RingHom   RingHom
        
 
 RingHom   RingHom
 
 
        |
20 | 16, 19 | syl6bb 265 |
. . . 4
     Sect    
 
 RingHom   RingHom
 
 
         |
21 | 14, 20 | anbi12d 716 |
. . 3
      Sect        Sect          RingHom 

RingHom    
         RingHom 

RingHom    
          |
22 | | anandi 836 |
. . 3
     RingHom

 RingHom   
          RingHom

 RingHom   
             RingHom   RingHom
 
 
        RingHom

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

 RingHom        RingHom   RingHom
 
 
       
          |
24 | | simplrl 769 |
. . . . . 6
      RingHom 

RingHom    
        RingHom

 RingHom        RingHom   RingHom
 
 
       
      

RingHom    |
25 | 24 | adantl 468 |
. . . . 5
 
     RingHom

 RingHom   
       
 RingHom   RingHom
       RingHom

 RingHom   
       
        

RingHom    |
26 | 11, 15 | rhmf 17947 |
. . . . . . . . . 10
  RingHom 
              |
27 | 15, 11 | rhmf 17947 |
. . . . . . . . . 10
  RingHom 
              |
28 | 26, 27 | anim12i 569 |
. . . . . . . . 9
   RingHom   RingHom
 
            
               |
29 | 28 | ad2antlr 732 |
. . . . . . . 8
      RingHom 

RingHom    
        RingHom

 RingHom        RingHom   RingHom
 
 
       
      
            
               |
30 | | simpr 463 |
. . . . . . . . 9
     RingHom

 RingHom   
       
                |
31 | 30 | adantl 468 |
. . . . . . . 8
      RingHom 

RingHom    
        RingHom

 RingHom        RingHom   RingHom
 
 
       
      
 
       |
32 | | simpr 463 |
. . . . . . . . 9
    RingHom   RingHom
 
 
       
       |
33 | 32 | ad2antrl 733 |
. . . . . . . 8
      RingHom 

RingHom    
        RingHom

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

RingHom    
        RingHom

 RingHom        RingHom   RingHom
 
 
       
      
             
            
 

      
         |
35 | 34 | adantl 468 |
. . . . . 6
 
     RingHom

 RingHom   
       
 RingHom   RingHom
       RingHom

 RingHom   
       
        
             
            
 

      
         |
36 | | fcof1o 6192 |
. . . . . . 7
                              
     
                     
   |
37 | | eqcom 2457 |
. . . . . . . 8
 
   |
38 | 37 | anbi2i 699 |
. . . . . . 7
             
 
            
    |
39 | 36, 38 | sylib 200 |
. . . . . 6
                              
     
                    
    |
40 | 35, 39 | syl 17 |
. . . . 5
 
     RingHom

 RingHom   
       
 RingHom   RingHom
       RingHom

 RingHom   
       
        
            
    |
41 | | anass 654 |
. . . . 5
    RingHom              
 
  RingHom
             
     |
42 | 25, 40, 41 | sylanbrc 669 |
. . . 4
 
     RingHom

 RingHom   
       
 RingHom   RingHom
       RingHom

 RingHom   
       
        
 
 RingHom                   |
43 | 11, 15 | isrim 17954 |
. . . . . . 7
 
   RingIso 
  RingHom
                 |
44 | 7, 8, 43 | syl2anc 666 |
. . . . . 6
   RingIso 
  RingHom
                 |
45 | 44 | anbi1d 710 |
. . . . 5
    RingIso

 
 
 RingHom                    |
46 | 45 | adantr 467 |
. . . 4
 
     RingHom

 RingHom   
       
 RingHom   RingHom
       RingHom

 RingHom   
       
        
 
 RingIso   
 
 RingHom                    |
47 | 42, 46 | mpbird 236 |
. . 3
 
     RingHom

 RingHom   
       
 RingHom   RingHom
       RingHom

 RingHom   
       
        
  RingIso

    |
48 | 11, 15 | rimrhm 17956 |
. . . . . 6
  RingIso 

RingHom    |
49 | 48 | ad2antrl 733 |
. . . . 5
 
  RingIso

  
 RingHom    |
50 | | isrim0 17944 |
. . . . . . . . . . 11
 
   RingIso 
  RingHom
 
 RingHom      |
51 | 7, 8, 50 | syl2anc 666 |
. . . . . . . . . 10
   RingIso 
  RingHom
 
 RingHom      |
52 | | eleq1 2516 |
. . . . . . . . . . . 12
     RingHom
  RingHom     |
53 | 52 | eqcoms 2458 |
. . . . . . . . . . 11
     RingHom
  RingHom     |
54 | 53 | anbi2d 709 |
. . . . . . . . . 10
     RingHom
 
 RingHom  
  RingHom

 RingHom      |
55 | 51, 54 | sylan9bbr 706 |
. . . . . . . . 9
    
 RingIso    RingHom

 RingHom      |
56 | | simpr 463 |
. . . . . . . . 9
   RingHom   RingHom
 

RingHom    |
57 | 55, 56 | syl6bi 232 |
. . . . . . . 8
    
 RingIso 

RingHom     |
58 | 57 | com12 32 |
. . . . . . 7
  RingIso 
 
   RingHom
    |
59 | 58 | expdimp 439 |
. . . . . 6
   RingIso      RingHom     |
60 | 59 | impcom 432 |
. . . . 5
 
  RingIso

  
 RingHom    |
61 | | coeq1 4991 |
. . . . . . 7
         |
62 | 61 | ad2antll 734 |
. . . . . 6
 
  RingIso

          |
63 | 11, 15 | rimf1o 17955 |
. . . . . . . 8
  RingIso 
              |
64 | 63 | ad2antrl 733 |
. . . . . . 7
 
  RingIso

                 |
65 | | f1ococnv1 5840 |
. . . . . . 7
               
       |
66 | 64, 65 | syl 17 |
. . . . . 6
 
  RingIso

     
       |
67 | 62, 66 | eqtrd 2484 |
. . . . 5
 
  RingIso

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

      RingHom

 RingHom   
         |
69 | 51 | biimpcd 228 |
. . . . . . 7
  RingIso 
   RingHom  
 RingHom      |
70 | 69 | adantr 467 |
. . . . . 6
   RingIso       RingHom
 
 RingHom      |
71 | 70 | impcom 432 |
. . . . 5
 
  RingIso

     RingHom  
 RingHom     |
72 | | eleq1 2516 |
. . . . . . 7
    RingHom 
  RingHom
    |
73 | 72 | ad2antll 734 |
. . . . . 6
 
  RingIso

     RingHom 
  RingHom
    |
74 | 73 | anbi2d 709 |
. . . . 5
 
  RingIso

      RingHom

 RingHom  
  RingHom
 
 RingHom      |
75 | 71, 74 | mpbird 236 |
. . . 4
 
  RingIso

     RingHom   RingHom
    |
76 | | coeq2 4992 |
. . . . . . 7
         |
77 | 76 | ad2antll 734 |
. . . . . 6
 
  RingIso

          |
78 | | f1ococnv2 5838 |
. . . . . . 7
               
       |
79 | 64, 78 | syl 17 |
. . . . . 6
 
  RingIso

     
       |
80 | 77, 79 | eqtrd 2484 |
. . . . 5
 
  RingIso

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

       RingHom 

RingHom    
       
        |
82 | 68, 75, 81 | jca31 537 |
. . 3
 
  RingIso

        RingHom   RingHom
 
 
        RingHom

 RingHom        RingHom   RingHom
 
 
       
         |
83 | 47, 82 | impbida 842 |
. 2
       RingHom   RingHom
 
 
        RingHom

 RingHom        RingHom   RingHom
 
 
       
         RingIso

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