Step | Hyp | Ref
| Expression |
1 | | fvex 5875 |
. . . . 5
     |
2 | 1 | a1i 11 |
. . . 4
       |
3 | | fvex 5875 |
. . . . . 6
     |
4 | 3 | a1i 11 |
. . . . 5
 
           |
5 | | fvex 5875 |
. . . . . . 7
Scalar   |
6 | 5 | a1i 11 |
. . . . . 6
       
    
Scalar    |
7 | | id 22 |
. . . . . . . . 9
 Scalar 
Scalar    |
8 | | simpll 760 |
. . . . . . . . . . 11
       
    
  |
9 | 8 | fveq2d 5869 |
. . . . . . . . . 10
       
    
Scalar  Scalar    |
10 | | isphl.f |
. . . . . . . . . 10
Scalar   |
11 | 9, 10 | syl6eqr 2503 |
. . . . . . . . 9
       
    
Scalar    |
12 | 7, 11 | sylan9eqr 2507 |
. . . . . . . 8
             
Scalar     |
13 | 12 | eleq1d 2513 |
. . . . . . 7
             
Scalar   
   |
14 | | simpllr 769 |
. . . . . . . . 9
             
Scalar         |
15 | | simplll 768 |
. . . . . . . . . . 11
             
Scalar     |
16 | 15 | fveq2d 5869 |
. . . . . . . . . 10
             
Scalar             |
17 | | isphl.v |
. . . . . . . . . 10
     |
18 | 16, 17 | syl6eqr 2503 |
. . . . . . . . 9
             
Scalar         |
19 | 14, 18 | eqtrd 2485 |
. . . . . . . 8
             
Scalar     |
20 | | simplr 762 |
. . . . . . . . . . . . 13
             
Scalar         |
21 | 15 | fveq2d 5869 |
. . . . . . . . . . . . . 14
             
Scalar             |
22 | | isphl.h |
. . . . . . . . . . . . . 14
     |
23 | 21, 22 | syl6eqr 2503 |
. . . . . . . . . . . . 13
             
Scalar        |
24 | 20, 23 | eqtrd 2485 |
. . . . . . . . . . . 12
             
Scalar    |
25 | 24 | oveqd 6307 |
. . . . . . . . . . 11
             
Scalar           |
26 | 19, 25 | mpteq12dv 4481 |
. . . . . . . . . 10
             
Scalar               |
27 | 12 | fveq2d 5869 |
. . . . . . . . . . 11
             
Scalar   ringLMod  ringLMod    |
28 | 15, 27 | oveq12d 6308 |
. . . . . . . . . 10
             
Scalar    LMHom ringLMod    LMHom ringLMod     |
29 | 26, 28 | eleq12d 2523 |
. . . . . . . . 9
             
Scalar           LMHom ringLMod        LMHom ringLMod      |
30 | 24 | oveqd 6307 |
. . . . . . . . . . 11
             
Scalar           |
31 | 12 | fveq2d 5869 |
. . . . . . . . . . . 12
             
Scalar             |
32 | | isphl.z |
. . . . . . . . . . . 12
     |
33 | 31, 32 | syl6eqr 2503 |
. . . . . . . . . . 11
             
Scalar         |
34 | 30, 33 | eqeq12d 2466 |
. . . . . . . . . 10
             
Scalar           
     |
35 | 15 | fveq2d 5869 |
. . . . . . . . . . . 12
             
Scalar             |
36 | | isphl.o |
. . . . . . . . . . . 12
     |
37 | 35, 36 | syl6eqr 2503 |
. . . . . . . . . . 11
             
Scalar        |
38 | 37 | eqeq2d 2461 |
. . . . . . . . . 10
             
Scalar       
  |
39 | 34, 38 | imbi12d 322 |
. . . . . . . . 9
             
Scalar                    
   |
40 | 12 | fveq2d 5869 |
. . . . . . . . . . . . 13
             
Scalar               |
41 | | isphl.i |
. . . . . . . . . . . . 13
      |
42 | 40, 41 | syl6eqr 2503 |
. . . . . . . . . . . 12
             
Scalar         |
43 | 24 | oveqd 6307 |
. . . . . . . . . . . 12
             
Scalar           |
44 | 42, 43 | fveq12d 5871 |
. . . . . . . . . . 11
             
Scalar                      |
45 | 44, 25 | eqeq12d 2466 |
. . . . . . . . . 10
             
Scalar                      
       |
46 | 19, 45 | raleqbidv 3001 |
. . . . . . . . 9
             
Scalar    
                 
         |
47 | 29, 39, 46 | 3anbi123d 1339 |
. . . . . . . 8
             
Scalar            LMHom ringLMod           
                              LMHom ringLMod     
           |
48 | 19, 47 | raleqbidv 3001 |
. . . . . . 7
             
Scalar    
        LMHom ringLMod           
                        
      LMHom ringLMod     
           |
49 | 13, 48 | anbi12d 717 |
. . . . . 6
             
Scalar              LMHom ringLMod           
                                 LMHom ringLMod      
           |
50 | 6, 49 | sbcied 3304 |
. . . . 5
       
    
  Scalar   ![]. ].](_drbrack.gif)           LMHom ringLMod                 
                           LMHom ringLMod     
            |
51 | 4, 50 | sbcied 3304 |
. . . 4
 
            ![]. ].](_drbrack.gif)  Scalar   ![]. ].](_drbrack.gif)           LMHom ringLMod           
                                 LMHom ringLMod      
           |
52 | 2, 51 | sbcied 3304 |
. . 3
        ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)  Scalar   ![]. ].](_drbrack.gif)  
        LMHom ringLMod  
                                          LMHom ringLMod      
           |
53 | | df-phl 19193 |
. . 3
       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)  Scalar   ![]. ].](_drbrack.gif)           LMHom ringLMod           
                           |
54 | 52, 53 | elrab2 3198 |
. 2
          LMHom ringLMod     
            |
55 | | 3anass 989 |
. 2
 

      LMHom ringLMod     

       



      LMHom ringLMod     

           |
56 | 54, 55 | bitr4i 256 |
1
  
      LMHom ringLMod  
 


          |