Step | Hyp | Ref
| Expression |
1 | | simp3 1010 |
. . 3
   LMHom  LFinGen LFinGen
LFinGen |
2 | | lmhmlmod2 18255 |
. . . . 5
  LMHom 
  |
3 | 2 | 3ad2ant1 1029 |
. . . 4
   LMHom  LFinGen LFinGen   |
4 | | lmhmrnlss 18273 |
. . . . 5
  LMHom 
      |
5 | 4 | 3ad2ant1 1029 |
. . . 4
   LMHom  LFinGen LFinGen       |
6 | | lmhmfgsplit.v |
. . . . 5

↾s   |
7 | | eqid 2451 |
. . . . 5
         |
8 | | eqid 2451 |
. . . . 5
         |
9 | 6, 7, 8 | islssfg 35928 |
. . . 4
       
LFinGen   
            |
10 | 3, 5, 9 | syl2anc 667 |
. . 3
   LMHom  LFinGen LFinGen  LFinGen
               |
11 | 1, 10 | mpbid 214 |
. 2
   LMHom  LFinGen LFinGen   
           |
12 | | simpl1 1011 |
. . . . 5
    LMHom 
LFinGen LFinGen  
           

LMHom    |
13 | | eqid 2451 |
. . . . . 6
         |
14 | | eqid 2451 |
. . . . . 6
         |
15 | 13, 14 | lmhmf 18257 |
. . . . 5
  LMHom 
              |
16 | | ffn 5728 |
. . . . 5
            
      |
17 | 12, 15, 16 | 3syl 18 |
. . . 4
    LMHom 
LFinGen LFinGen  
           
      |
18 | | elpwi 3960 |
. . . . 5
 
  |
19 | 18 | ad2antrl 734 |
. . . 4
    LMHom 
LFinGen LFinGen  
           
  |
20 | | simprrl 774 |
. . . 4
    LMHom 
LFinGen LFinGen  
           
  |
21 | | fipreima 7880 |
. . . 4
     
                |
22 | 17, 19, 20, 21 | syl3anc 1268 |
. . 3
    LMHom 
LFinGen LFinGen  
           
               |
23 | | eqid 2451 |
. . . . . . 7
         |
24 | | eqid 2451 |
. . . . . . 7
         |
25 | | lmhmfgsplit.z |
. . . . . . 7
     |
26 | | lmhmfgsplit.k |
. . . . . . 7
      |
27 | | simpll1 1047 |
. . . . . . 7
     LMHom  LFinGen LFinGen                            
 LMHom    |
28 | | lmhmlmod1 18256 |
. . . . . . . . . 10
  LMHom 
  |
29 | 28 | 3ad2ant1 1029 |
. . . . . . . . 9
   LMHom  LFinGen LFinGen   |
30 | 29 | ad2antrr 732 |
. . . . . . . 8
     LMHom  LFinGen LFinGen                            
  |
31 | | inss1 3652 |
. . . . . . . . . . 11
     
       |
32 | 31 | sseli 3428 |
. . . . . . . . . 10
               |
33 | | elpwi 3960 |
. . . . . . . . . 10
            |
34 | 32, 33 | syl 17 |
. . . . . . . . 9
              |
35 | 34 | ad2antrl 734 |
. . . . . . . 8
     LMHom  LFinGen LFinGen                            
      |
36 | | eqid 2451 |
. . . . . . . . 9
         |
37 | 13, 23, 36 | lspcl 18199 |
. . . . . . . 8
                     |
38 | 30, 35, 37 | syl2anc 667 |
. . . . . . 7
     LMHom  LFinGen LFinGen                                           |
39 | 13, 36, 8 | lmhmlsp 18272 |
. . . . . . . . 9
   LMHom                                 |
40 | 27, 35, 39 | syl2anc 667 |
. . . . . . . 8
     LMHom  LFinGen LFinGen                                                       |
41 | | fveq2 5865 |
. . . . . . . . 9
                           |
42 | 41 | ad2antll 735 |
. . . . . . . 8
     LMHom  LFinGen LFinGen                                                   |
43 | | simp2rr 1078 |
. . . . . . . . 9
    LMHom 
LFinGen LFinGen  
                                   |
44 | 43 | 3expa 1208 |
. . . . . . . 8
     LMHom  LFinGen LFinGen                                       |
45 | 40, 42, 44 | 3eqtrd 2489 |
. . . . . . 7
     LMHom  LFinGen LFinGen                                           |
46 | 23, 24, 25, 26, 13, 27, 38, 45 | kercvrlsm 35941 |
. . . . . 6
     LMHom  LFinGen LFinGen                                                   |
47 | 46 | oveq2d 6306 |
. . . . 5
     LMHom  LFinGen LFinGen                             
↾s                   ↾s        |
48 | 13 | ressid 15184 |
. . . . . . 7

 ↾s        |
49 | 29, 48 | syl 17 |
. . . . . 6
   LMHom  LFinGen LFinGen 
↾s        |
50 | 49 | ad2antrr 732 |
. . . . 5
     LMHom  LFinGen LFinGen                             
↾s        |
51 | 47, 50 | eqtr2d 2486 |
. . . 4
     LMHom  LFinGen LFinGen                            
 ↾s                    |
52 | | lmhmfgsplit.u |
. . . . 5

↾s   |
53 | | eqid 2451 |
. . . . 5
 ↾s          
↾s           |
54 | | eqid 2451 |
. . . . 5
 ↾s                  
↾s                   |
55 | 26, 25, 23 | lmhmkerlss 18274 |
. . . . . . 7
  LMHom 
      |
56 | 55 | 3ad2ant1 1029 |
. . . . . 6
   LMHom  LFinGen LFinGen       |
57 | 56 | ad2antrr 732 |
. . . . 5
     LMHom  LFinGen LFinGen                            
      |
58 | | simpll2 1048 |
. . . . 5
     LMHom  LFinGen LFinGen                            
LFinGen |
59 | | inss2 3653 |
. . . . . . . 8
     
  |
60 | 59 | sseli 3428 |
. . . . . . 7
          |
61 | 60 | ad2antrl 734 |
. . . . . 6
     LMHom  LFinGen LFinGen                               |
62 | 36, 13, 53 | islssfgi 35930 |
. . . . . 6
     

 ↾s          LFinGen |
63 | 30, 35, 61, 62 | syl3anc 1268 |
. . . . 5
     LMHom  LFinGen LFinGen                             
↾s          LFinGen |
64 | 23, 24, 52, 53, 54, 30, 57, 38, 58, 63 | lsmfgcl 35932 |
. . . 4
     LMHom  LFinGen LFinGen                             
↾s                  LFinGen |
65 | 51, 64 | eqeltrd 2529 |
. . 3
     LMHom  LFinGen LFinGen                            
LFinGen |
66 | 22, 65 | rexlimddv 2883 |
. 2
    LMHom 
LFinGen LFinGen  
           
LFinGen |
67 | 11, 66 | rexlimddv 2883 |
1
   LMHom  LFinGen LFinGen
LFinGen |