Step | Hyp | Ref
| Expression |
1 | | ringcvalALTV.c |
. 2
RingCatALTV   |
2 | | df-ringcALTV 40333 |
. . . 4
RingCatALTV   
  ![]_ ]_](_urbrack.gif)       
      
   RingHom      comp             RingHom        RingHom              |
3 | 2 | a1i 11 |
. . 3
 RingCatALTV      ![]_ ]_](_urbrack.gif)       
      
   RingHom      comp             RingHom        RingHom               |
4 | | vex 3016 |
. . . . . 6
 |
5 | 4 | inex1 4516 |
. . . . 5
   |
6 | 5 | a1i 11 |
. . . 4
 
 
   |
7 | | ineq1 3595 |
. . . . . 6
 
     |
8 | 7 | adantl 472 |
. . . . 5
 
 
     |
9 | | ringcvalALTV.b |
. . . . . 6
     |
10 | 9 | adantr 471 |
. . . . 5
 
     |
11 | 8, 10 | eqtr4d 2489 |
. . . 4
 
 
   |
12 | | simpr 467 |
. . . . . 6
       |
13 | 12 | opeq2d 4143 |
. . . . 5
           
         |
14 | | eqidd 2453 |
. . . . . . . 8
      RingHom   RingHom    |
15 | 12, 12, 14 | mpt2eq123dv 6341 |
. . . . . . 7
        RingHom      RingHom     |
16 | | ringcvalALTV.h |
. . . . . . . 8
    RingHom     |
17 | 16 | ad2antrr 737 |
. . . . . . 7
        RingHom     |
18 | 15, 17 | eqtr4d 2489 |
. . . . . 6
        RingHom     |
19 | 18 | opeq2d 4143 |
. . . . 5
             RingHom   
        |
20 | 12 | sqxpeqd 4838 |
. . . . . . . 8
           |
21 | | eqidd 2453 |
. . . . . . . 8
           RingHom        RingHom               RingHom        RingHom           |
22 | 20, 12, 21 | mpt2eq123dv 6341 |
. . . . . . 7
               RingHom        RingHom                    RingHom        RingHom            |
23 | | ringcvalALTV.o |
. . . . . . . 8
           RingHom        RingHom            |
24 | 23 | ad2antrr 737 |
. . . . . . 7
               RingHom        RingHom            |
25 | 22, 24 | eqtr4d 2489 |
. . . . . 6
               RingHom        RingHom           |
26 | 25 | opeq2d 4143 |
. . . . 5
      comp             RingHom        RingHom            comp     |
27 | 13, 19, 26 | tpeq123d 4035 |
. . . 4
                      RingHom      comp             RingHom        RingHom                  
      
   comp      |
28 | 6, 11, 27 | csbied2 3359 |
. . 3
 
  
  ![]_ ]_](_urbrack.gif)                  RingHom      comp             RingHom        RingHom                  
      
   comp      |
29 | | ringcvalALTV.u |
. . . 4
   |
30 | | elex 3022 |
. . . 4
   |
31 | 29, 30 | syl 17 |
. . 3
   |
32 | | tpex 6578 |
. . . 4
                 comp   
 |
33 | 32 | a1i 11 |
. . 3
       
      
   comp      |
34 | 3, 28, 31, 33 | fvmptd 5938 |
. 2
 RingCatALTV        
      
   comp      |
35 | 1, 34 | syl5eq 2498 |
1
                  comp      |