Step | Hyp | Ref
| Expression |
1 | | lmhmlmod1 18304 |
. . 3
  LMHom 
  |
2 | 1 | 3ad2ant1 1035 |
. 2
   LMHom  LNoeM LNoeM   |
3 | | eqid 2461 |
. . . . . 6
         |
4 | | eqid 2461 |
. . . . . 6
 ↾s   ↾s   |
5 | 3, 4 | reslmhm 18323 |
. . . . 5
   LMHom      
   
↾s  LMHom    |
6 | 5 | 3ad2antl1 1176 |
. . . 4
    LMHom 
LNoeM LNoeM
    
   
↾s  LMHom    |
7 | | cnvresima 5342 |
. . . . . . . 8
               |
8 | | lmhmfgsplit.k |
. . . . . . . . . 10
      |
9 | 8 | eqcomi 2470 |
. . . . . . . . 9
      |
10 | 9 | ineq1i 3641 |
. . . . . . . 8
          |
11 | | incom 3636 |
. . . . . . . 8
     |
12 | 7, 10, 11 | 3eqtri 2487 |
. . . . . . 7
          |
13 | 12 | oveq2i 6325 |
. . . . . 6
  ↾s 
↾s   
  
    ↾s 
↾s     |
14 | | lmhmfgsplit.u |
. . . . . . . . 9

↾s   |
15 | 14 | oveq1i 6324 |
. . . . . . . 8
 ↾s      ↾s 
↾s     |
16 | | simpl1 1017 |
. . . . . . . . . 10
    LMHom 
LNoeM LNoeM
    

LMHom    |
17 | | cnvexg 6765 |
. . . . . . . . . . . 12
  LMHom 
   |
18 | | imaexg 6756 |
. . . . . . . . . . . 12
         |
19 | 17, 18 | syl 17 |
. . . . . . . . . . 11
  LMHom 
       |
20 | 8, 19 | syl5eqel 2543 |
. . . . . . . . . 10
  LMHom 
  |
21 | 16, 20 | syl 17 |
. . . . . . . . 9
    LMHom 
LNoeM LNoeM
    
  |
22 | | inss2 3664 |
. . . . . . . . 9
   |
23 | | ressabs 15236 |
. . . . . . . . 9
   
   ↾s  ↾s     ↾s      |
24 | 21, 22, 23 | sylancl 673 |
. . . . . . . 8
    LMHom 
LNoeM LNoeM
    
  ↾s 
↾s    
↾s      |
25 | 15, 24 | syl5eq 2507 |
. . . . . . 7
    LMHom 
LNoeM LNoeM
    
 ↾s 
   ↾s      |
26 | | vex 3059 |
. . . . . . . 8
 |
27 | | inss1 3663 |
. . . . . . . 8
   |
28 | | ressabs 15236 |
. . . . . . . 8
   
   ↾s  ↾s     ↾s      |
29 | 26, 27, 28 | mp2an 683 |
. . . . . . 7
  ↾s 
↾s    
↾s     |
30 | 25, 29 | syl6reqr 2514 |
. . . . . 6
    LMHom 
LNoeM LNoeM
    
  ↾s 
↾s    
↾s      |
31 | 13, 30 | syl5eq 2507 |
. . . . 5
    LMHom 
LNoeM LNoeM
    
  ↾s 
↾s   
  
   ↾s      |
32 | | simpl2 1018 |
. . . . . 6
    LMHom 
LNoeM LNoeM
    
LNoeM |
33 | 2 | adantr 471 |
. . . . . . . 8
    LMHom 
LNoeM LNoeM
    
  |
34 | | simpr 467 |
. . . . . . . 8
    LMHom 
LNoeM LNoeM
    
      |
35 | | lmhmfgsplit.z |
. . . . . . . . . 10
     |
36 | 8, 35, 3 | lmhmkerlss 18322 |
. . . . . . . . 9
  LMHom 
      |
37 | 16, 36 | syl 17 |
. . . . . . . 8
    LMHom 
LNoeM LNoeM
    
      |
38 | 3 | lssincl 18236 |
. . . . . . . 8
     
             |
39 | 33, 34, 37, 38 | syl3anc 1276 |
. . . . . . 7
    LMHom 
LNoeM LNoeM
    
        |
40 | 22 | a1i 11 |
. . . . . . 7
    LMHom 
LNoeM LNoeM
    
    |
41 | | eqid 2461 |
. . . . . . . . 9
         |
42 | 14, 3, 41 | lsslss 18232 |
. . . . . . . 8
      
 
            
     |
43 | 33, 37, 42 | syl2anc 671 |
. . . . . . 7
    LMHom 
LNoeM LNoeM
    
 
            
     |
44 | 39, 40, 43 | mpbir2and 938 |
. . . . . 6
    LMHom 
LNoeM LNoeM
    
        |
45 | | eqid 2461 |
. . . . . . 7
 ↾s     ↾s     |
46 | 41, 45 | lnmlssfg 35982 |
. . . . . 6
  LNoeM

     
 ↾s 
 
LFinGen |
47 | 32, 44, 46 | syl2anc 671 |
. . . . 5
    LMHom 
LNoeM LNoeM
    
 ↾s 
 
LFinGen |
48 | 31, 47 | eqeltrd 2539 |
. . . 4
    LMHom 
LNoeM LNoeM
    
  ↾s 
↾s   
  
 
LFinGen |
49 | | lmhmfgsplit.v |
. . . . . . . . 9

↾s   |
50 | 49 | oveq1i 6324 |
. . . . . . . 8
 ↾s     
↾s  ↾s     |
51 | | rnexg 6751 |
. . . . . . . . 9
  LMHom 
  |
52 | | resexg 5165 |
. . . . . . . . . 10
  LMHom 
    |
53 | | rnexg 6751 |
. . . . . . . . . 10
 

    |
54 | 52, 53 | syl 17 |
. . . . . . . . 9
  LMHom 
    |
55 | | ressress 15235 |
. . . . . . . . 9
       ↾s 
↾s    
↾s        |
56 | 51, 54, 55 | syl2anc 671 |
. . . . . . . 8
  LMHom 
  ↾s 
↾s    
↾s        |
57 | 50, 56 | syl5eq 2507 |
. . . . . . 7
  LMHom 
 ↾s 
   ↾s  
     |
58 | | incom 3636 |
. . . . . . . . 9

        |
59 | | resss 5146 |
. . . . . . . . . . 11
   |
60 | | rnss 5081 |
. . . . . . . . . . 11
 

    |
61 | 59, 60 | ax-mp 5 |
. . . . . . . . . 10
   |
62 | | df-ss 3429 |
. . . . . . . . . 10
  
 

     |
63 | 61, 62 | mpbi 213 |
. . . . . . . . 9
  
    |
64 | 58, 63 | eqtr2i 2484 |
. . . . . . . 8
       |
65 | 64 | oveq2i 6325 |
. . . . . . 7
 ↾s     ↾s       |
66 | 57, 65 | syl6reqr 2514 |
. . . . . 6
  LMHom 
 ↾s 
   ↾s      |
67 | 16, 66 | syl 17 |
. . . . 5
    LMHom 
LNoeM LNoeM
    
 ↾s 
   ↾s      |
68 | | simpl3 1019 |
. . . . . 6
    LMHom 
LNoeM LNoeM
    
LNoeM |
69 | | lmhmrnlss 18321 |
. . . . . . . 8
 
   ↾s  LMHom  
       |
70 | 6, 69 | syl 17 |
. . . . . . 7
    LMHom 
LNoeM LNoeM
    
        |
71 | 61 | a1i 11 |
. . . . . . 7
    LMHom 
LNoeM LNoeM
    
    |
72 | | lmhmlmod2 18303 |
. . . . . . . . 9
  LMHom 
  |
73 | 16, 72 | syl 17 |
. . . . . . . 8
    LMHom 
LNoeM LNoeM
    
  |
74 | | lmhmrnlss 18321 |
. . . . . . . . 9
  LMHom 
      |
75 | 16, 74 | syl 17 |
. . . . . . . 8
    LMHom 
LNoeM LNoeM
    
      |
76 | | eqid 2461 |
. . . . . . . . 9
         |
77 | | eqid 2461 |
. . . . . . . . 9
         |
78 | 49, 76, 77 | lsslss 18232 |
. . . . . . . 8
             
 
    
      |
79 | 73, 75, 78 | syl2anc 671 |
. . . . . . 7
    LMHom 
LNoeM LNoeM
    
 
                  |
80 | 70, 71, 79 | mpbir2and 938 |
. . . . . 6
    LMHom 
LNoeM LNoeM
    
        |
81 | | eqid 2461 |
. . . . . . 7
 ↾s     ↾s     |
82 | 77, 81 | lnmlssfg 35982 |
. . . . . 6
  LNoeM
      
 ↾s 
 
LFinGen |
83 | 68, 80, 82 | syl2anc 671 |
. . . . 5
    LMHom 
LNoeM LNoeM
    
 ↾s 
 
LFinGen |
84 | 67, 83 | eqeltrd 2539 |
. . . 4
    LMHom 
LNoeM LNoeM
    
 ↾s 
 
LFinGen |
85 | | eqid 2461 |
. . . . 5
               |
86 | | eqid 2461 |
. . . . 5
  ↾s 
↾s   
  
    ↾s 
↾s   
  
   |
87 | | eqid 2461 |
. . . . 5
 ↾s     ↾s     |
88 | 35, 85, 86, 87 | lmhmfgsplit 35988 |
. . . 4
      ↾s  LMHom    ↾s  ↾s         LFinGen 
↾s    LFinGen  ↾s  LFinGen |
89 | 6, 48, 84, 88 | syl3anc 1276 |
. . 3
    LMHom 
LNoeM LNoeM
    
 ↾s 
LFinGen |
90 | 89 | ralrimiva 2813 |
. 2
   LMHom  LNoeM LNoeM        ↾s  LFinGen |
91 | 3 | islnm 35979 |
. 2
 LNoeM         ↾s  LFinGen  |
92 | 2, 90, 91 | sylanbrc 675 |
1
   LMHom  LNoeM LNoeM LNoeM |