Step | Hyp | Ref
| Expression |
1 | | eqid 2451 |
. . 3
       |
2 | | pj1lmhm.s |
. . 3
     |
3 | | pj1lmhm.z |
. . 3
     |
4 | | eqid 2451 |
. . 3
Cntz  Cntz   |
5 | | pj1lmhm.1 |
. . . . 5
   |
6 | | pj1lmhm.l |
. . . . . 6
     |
7 | 6 | lsssssubg 18181 |
. . . . 5

SubGrp    |
8 | 5, 7 | syl 17 |
. . . 4

SubGrp    |
9 | | pj1lmhm.2 |
. . . 4
   |
10 | 8, 9 | sseldd 3433 |
. . 3
 SubGrp    |
11 | | pj1lmhm.3 |
. . . 4
   |
12 | 8, 11 | sseldd 3433 |
. . 3
 SubGrp    |
13 | | pj1lmhm.4 |
. . 3
     |
14 | | lmodabl 18135 |
. . . . 5

  |
15 | 5, 14 | syl 17 |
. . . 4
   |
16 | 4, 15, 10, 12 | ablcntzd 17495 |
. . 3

 Cntz       |
17 | | pj1lmhm.p |
. . 3
      |
18 | 1, 2, 3, 4, 10, 12, 13, 16, 17 | pj1ghm 17353 |
. 2
       ↾s       |
19 | | eqid 2451 |
. . 3
Scalar  Scalar   |
20 | 19 | a1i 11 |
. 2
 Scalar  Scalar    |
21 | 1, 2, 3, 4, 10, 12, 13, 16, 17 | pj1id 17349 |
. . . . . . . . 9
 

 
                         |
22 | 21 | adantrl 722 |
. . . . . . . 8
 
    Scalar  
                             |
23 | 22 | oveq2d 6306 |
. . . . . . 7
 
    Scalar  
                                             |
24 | 5 | adantr 467 |
. . . . . . . 8
 
    Scalar  
      |
25 | | simprl 764 |
. . . . . . . 8
 
    Scalar  
       Scalar     |
26 | 9 | adantr 467 |
. . . . . . . . . 10
 
    Scalar  
      |
27 | | eqid 2451 |
. . . . . . . . . . 11
         |
28 | 27, 6 | lssss 18160 |
. . . . . . . . . 10
       |
29 | 26, 28 | syl 17 |
. . . . . . . . 9
 
    Scalar  
          |
30 | 10 | adantr 467 |
. . . . . . . . . . 11
 
    Scalar  
    SubGrp    |
31 | 12 | adantr 467 |
. . . . . . . . . . 11
 
    Scalar  
    SubGrp    |
32 | 13 | adantr 467 |
. . . . . . . . . . 11
 
    Scalar  
        |
33 | 16 | adantr 467 |
. . . . . . . . . . 11
 
    Scalar  
     Cntz       |
34 | 1, 2, 3, 4, 30, 31, 32, 33, 17 | pj1f 17347 |
. . . . . . . . . 10
 
    Scalar  
          
     |
35 | | simprr 766 |
. . . . . . . . . 10
 
    Scalar  
    
   |
36 | 34, 35 | ffvelrnd 6023 |
. . . . . . . . 9
 
    Scalar  
              |
37 | 29, 36 | sseldd 3433 |
. . . . . . . 8
 
    Scalar  
                  |
38 | 11 | adantr 467 |
. . . . . . . . . 10
 
    Scalar  
      |
39 | 27, 6 | lssss 18160 |
. . . . . . . . . 10
       |
40 | 38, 39 | syl 17 |
. . . . . . . . 9
 
    Scalar  
          |
41 | 1, 2, 3, 4, 30, 31, 32, 33, 17 | pj2f 17348 |
. . . . . . . . . 10
 
    Scalar  
          
     |
42 | 41, 35 | ffvelrnd 6023 |
. . . . . . . . 9
 
    Scalar  
              |
43 | 40, 42 | sseldd 3433 |
. . . . . . . 8
 
    Scalar  
                  |
44 | | eqid 2451 |
. . . . . . . . 9
         |
45 | | eqid 2451 |
. . . . . . . . 9
   Scalar      Scalar    |
46 | 27, 1, 19, 44, 45 | lmodvsdi 18114 |
. . . . . . . 8
      Scalar  
                                                                                                  |
47 | 24, 25, 37, 43, 46 | syl13anc 1270 |
. . . . . . 7
 
    Scalar  
                                                                            |
48 | 23, 47 | eqtrd 2485 |
. . . . . 6
 
    Scalar  
                                                     |
49 | 6, 2 | lsmcl 18306 |
. . . . . . . . . 10
 
     |
50 | 5, 9, 11, 49 | syl3anc 1268 |
. . . . . . . . 9
     |
51 | 50 | adantr 467 |
. . . . . . . 8
 
    Scalar  
        |
52 | 19, 44, 45, 6 | lssvscl 18178 |
. . . . . . . 8
      
   Scalar                   |
53 | 24, 51, 25, 35, 52 | syl22anc 1269 |
. . . . . . 7
 
    Scalar  
            
   |
54 | 19, 44, 45, 6 | lssvscl 18178 |
. . . . . . . 8
        Scalar            
                  |
55 | 24, 26, 25, 36, 54 | syl22anc 1269 |
. . . . . . 7
 
    Scalar  
                      |
56 | 19, 44, 45, 6 | lssvscl 18178 |
. . . . . . . 8
        Scalar            
                  |
57 | 24, 38, 25, 42, 56 | syl22anc 1269 |
. . . . . . 7
 
    Scalar  
                      |
58 | 1, 2, 3, 4, 30, 31, 32, 33, 17, 53, 55, 57 | pj1eq 17350 |
. . . . . 6
 
    Scalar  
                                                                                                                         |
59 | 48, 58 | mpbid 214 |
. . . . 5
 
    Scalar  
                                                                        |
60 | 59 | simpld 461 |
. . . 4
 
    Scalar  
                                      |
61 | 60 | ralrimivva 2809 |
. . 3
     Scalar                                          |
62 | 8, 50 | sseldd 3433 |
. . . . . 6
   SubGrp    |
63 | | eqid 2451 |
. . . . . . 7
 ↾s 
   ↾s 
   |
64 | 63 | subgbas 16821 |
. . . . . 6
 
 SubGrp        ↾s 
     |
65 | 62, 64 | syl 17 |
. . . . 5
       ↾s 
     |
66 | 65 | raleqdv 2993 |
. . . 4
                                     
     ↾s 
                                       |
67 | 66 | ralbidv 2827 |
. . 3
      Scalar    
                                       Scalar         ↾s 
                                       |
68 | 61, 67 | mpbid 214 |
. 2
     Scalar         ↾s 
                                      |
69 | 63, 6 | lsslmod 18183 |
. . . 4
      ↾s 
    |
70 | 5, 50, 69 | syl2anc 667 |
. . 3
 
↾s      |
71 | | ovex 6318 |
. . . . 5
   |
72 | 63, 19 | resssca 15275 |
. . . . 5
 

Scalar  Scalar 
↾s       |
73 | 71, 72 | ax-mp 5 |
. . . 4
Scalar  Scalar 
↾s      |
74 | | eqid 2451 |
. . . 4
   
↾s         ↾s 
    |
75 | 63, 44 | ressvsca 15276 |
. . . . 5
 

        ↾s 
     |
76 | 71, 75 | ax-mp 5 |
. . . 4
        ↾s 
    |
77 | 73, 19, 45, 74, 76, 44 | islmhm3 18251 |
. . 3
  
↾s           
↾s    LMHom        
↾s     Scalar  Scalar  
   Scalar         ↾s 
                                        |
78 | 70, 5, 77 | syl2anc 667 |
. 2
       
↾s    LMHom        
↾s     Scalar  Scalar  
   Scalar         ↾s 
                                        |
79 | 18, 20, 68, 78 | mpbir3and 1191 |
1
       ↾s    LMHom    |