Step | Hyp | Ref
| Expression |
1 | | mendassa.a |
. . . 4
MEndo   |
2 | 1 | mendbas 36121 |
. . 3
 LMHom       |
3 | 2 | a1i 11 |
. 2

 LMHom        |
4 | | eqidd 2472 |
. 2

        |
5 | | eqidd 2472 |
. 2

          |
6 | | eqid 2471 |
. . . . . 6
       |
7 | | eqid 2471 |
. . . . . 6
       |
8 | 1, 2, 6, 7 | mendplusg 36123 |
. . . . 5
   LMHom   LMHom  
  
              |
9 | 6 | lmhmplusg 18345 |
. . . . 5
   LMHom   LMHom  
         LMHom    |
10 | 8, 9 | eqeltrd 2549 |
. . . 4
   LMHom   LMHom  
  
     LMHom    |
11 | 10 | 3adant1 1048 |
. . 3
   LMHom   LMHom           LMHom    |
12 | | simpr1 1036 |
. . . . . 6
    LMHom   LMHom   LMHom   

LMHom    |
13 | | simpr2 1037 |
. . . . . 6
    LMHom   LMHom   LMHom   

LMHom    |
14 | 12, 13, 9 | syl2anc 673 |
. . . . 5
    LMHom   LMHom   LMHom   
         LMHom    |
15 | | simpr3 1038 |
. . . . 5
    LMHom   LMHom   LMHom   

LMHom    |
16 | 1, 2, 6, 7 | mendplusg 36123 |
. . . . 5
           LMHom   LMHom                                    |
17 | 14, 15, 16 | syl2anc 673 |
. . . 4
    LMHom   LMHom   LMHom   
                                 |
18 | 12, 13, 8 | syl2anc 673 |
. . . . 5
    LMHom   LMHom   LMHom   
  
              |
19 | 18 | oveq1d 6323 |
. . . 4
    LMHom   LMHom   LMHom   
                               |
20 | 6 | lmhmplusg 18345 |
. . . . . . 7
   LMHom   LMHom  
         LMHom    |
21 | 13, 15, 20 | syl2anc 673 |
. . . . . 6
    LMHom   LMHom   LMHom   
         LMHom    |
22 | 1, 2, 6, 7 | mendplusg 36123 |
. . . . . 6
   LMHom           LMHom                                    |
23 | 12, 21, 22 | syl2anc 673 |
. . . . 5
    LMHom   LMHom   LMHom   
  
                              |
24 | 1, 2, 6, 7 | mendplusg 36123 |
. . . . . . 7
   LMHom   LMHom  
  
              |
25 | 13, 15, 24 | syl2anc 673 |
. . . . . 6
    LMHom   LMHom   LMHom   
  
              |
26 | 25 | oveq2d 6324 |
. . . . 5
    LMHom   LMHom   LMHom   
  
                            |
27 | | lmodgrp 18176 |
. . . . . . . 8

  |
28 | | grpmnd 16756 |
. . . . . . . 8
   |
29 | 27, 28 | syl 17 |
. . . . . . 7

  |
30 | 29 | adantr 472 |
. . . . . 6
    LMHom   LMHom   LMHom   
  |
31 | | eqid 2471 |
. . . . . . . . 9
         |
32 | 31, 31 | lmhmf 18335 |
. . . . . . . 8
  LMHom 
              |
33 | 12, 32 | syl 17 |
. . . . . . 7
    LMHom   LMHom   LMHom   
              |
34 | | fvex 5889 |
. . . . . . . 8
     |
35 | 34, 34 | elmap 7518 |
. . . . . . 7
                         |
36 | 33, 35 | sylibr 217 |
. . . . . 6
    LMHom   LMHom   LMHom   
    
       |
37 | 31, 31 | lmhmf 18335 |
. . . . . . . 8
  LMHom 
              |
38 | 13, 37 | syl 17 |
. . . . . . 7
    LMHom   LMHom   LMHom   
              |
39 | 34, 34 | elmap 7518 |
. . . . . . 7
                         |
40 | 38, 39 | sylibr 217 |
. . . . . 6
    LMHom   LMHom   LMHom   
    
       |
41 | 31, 31 | lmhmf 18335 |
. . . . . . . 8
  LMHom 
              |
42 | 15, 41 | syl 17 |
. . . . . . 7
    LMHom   LMHom   LMHom   
              |
43 | 34, 34 | elmap 7518 |
. . . . . . 7
                         |
44 | 42, 43 | sylibr 217 |
. . . . . 6
    LMHom   LMHom   LMHom   
    
       |
45 | 31, 6 | mndvass 19494 |
. . . . . 6
  
              
    
                                              |
46 | 30, 36, 40, 44, 45 | syl13anc 1294 |
. . . . 5
    LMHom   LMHom   LMHom   
                                  |
47 | 23, 26, 46 | 3eqtr4d 2515 |
. . . 4
    LMHom   LMHom   LMHom   
  
                             |
48 | 17, 19, 47 | 3eqtr4d 2515 |
. . 3
    LMHom   LMHom   LMHom   
                              |
49 | | id 22 |
. . . 4

  |
50 | | eqidd 2472 |
. . . 4

Scalar  Scalar    |
51 | | eqid 2471 |
. . . . 5
         |
52 | | eqid 2471 |
. . . . 5
Scalar  Scalar   |
53 | 51, 31, 52, 52 | 0lmhm 18341 |
. . . 4
 
Scalar  Scalar                LMHom    |
54 | 49, 49, 50, 53 | syl3anc 1292 |
. . 3

             LMHom    |
55 | 1, 2, 6, 7 | mendplusg 36123 |
. . . . 5
               LMHom 
 LMHom                                            |
56 | 54, 55 | sylan 479 |
. . . 4
   LMHom  
                                         |
57 | 32, 35 | sylibr 217 |
. . . . 5
  LMHom 
    
       |
58 | 31, 6, 51 | mndvlid 19495 |
. . . . 5
 
                                 |
59 | 29, 57, 58 | syl2an 485 |
. . . 4
   LMHom  
                      |
60 | 56, 59 | eqtrd 2505 |
. . 3
   LMHom  
                     |
61 | | eqid 2471 |
. . . . 5
           |
62 | 61 | invlmhm 18343 |
. . . 4

      LMHom    |
63 | | lmhmco 18344 |
. . . 4
        LMHom 
 LMHom           LMHom    |
64 | 62, 63 | sylan 479 |
. . 3
   LMHom  
        LMHom    |
65 | 1, 2, 6, 7 | mendplusg 36123 |
. . . . 5
          LMHom   LMHom  
                               |
66 | 64, 65 | sylancom 680 |
. . . 4
   LMHom  
                               |
67 | 31, 6, 61, 51 | grpvlinv 19497 |
. . . . 5
 
                                        |
68 | 27, 57, 67 | syl2an 485 |
. . . 4
   LMHom  
                             |
69 | 66, 68 | eqtrd 2505 |
. . 3
   LMHom  
                            |
70 | 3, 4, 11, 48, 54, 60, 64, 69 | isgrpd 16769 |
. 2

  |
71 | | eqid 2471 |
. . . . 5
         |
72 | 1, 2, 71 | mendmulr 36125 |
. . . 4
   LMHom   LMHom  
            |
73 | | lmhmco 18344 |
. . . 4
   LMHom   LMHom  
   LMHom    |
74 | 72, 73 | eqeltrd 2549 |
. . 3
   LMHom   LMHom  
         LMHom    |
75 | 74 | 3adant1 1048 |
. 2
   LMHom   LMHom            LMHom    |
76 | | coass 5361 |
. . 3
         |
77 | 12, 13, 72 | syl2anc 673 |
. . . . 5
    LMHom   LMHom   LMHom   
            |
78 | 77 | oveq1d 6323 |
. . . 4
    LMHom   LMHom   LMHom   
                            |
79 | 12, 13, 73 | syl2anc 673 |
. . . . 5
    LMHom   LMHom   LMHom   
   LMHom    |
80 | 1, 2, 71 | mendmulr 36125 |
. . . . 5
     LMHom   LMHom  
                |
81 | 79, 15, 80 | syl2anc 673 |
. . . 4
    LMHom   LMHom   LMHom   
                |
82 | 78, 81 | eqtrd 2505 |
. . 3
    LMHom   LMHom   LMHom   
                      |
83 | 1, 2, 71 | mendmulr 36125 |
. . . . . 6
   LMHom   LMHom  
            |
84 | 13, 15, 83 | syl2anc 673 |
. . . . 5
    LMHom   LMHom   LMHom   
            |
85 | 84 | oveq2d 6324 |
. . . 4
    LMHom   LMHom   LMHom   
                            |
86 | | lmhmco 18344 |
. . . . . 6
   LMHom   LMHom  
   LMHom    |
87 | 13, 15, 86 | syl2anc 673 |
. . . . 5
    LMHom   LMHom   LMHom   
   LMHom    |
88 | 1, 2, 71 | mendmulr 36125 |
. . . . 5
   LMHom     LMHom                   |
89 | 12, 87, 88 | syl2anc 673 |
. . . 4
    LMHom   LMHom   LMHom   
                |
90 | 85, 89 | eqtrd 2505 |
. . 3
    LMHom   LMHom   LMHom   
                      |
91 | 76, 82, 90 | 3eqtr4a 2531 |
. 2
    LMHom   LMHom   LMHom   
                                  |
92 | 1, 2, 71 | mendmulr 36125 |
. . . 4
   LMHom           LMHom                               |
93 | 12, 21, 92 | syl2anc 673 |
. . 3
    LMHom   LMHom   LMHom   
                            |
94 | 25 | oveq2d 6324 |
. . 3
    LMHom   LMHom   LMHom   
                                 |
95 | | lmhmco 18344 |
. . . . . 6
   LMHom   LMHom  
   LMHom    |
96 | 12, 15, 95 | syl2anc 673 |
. . . . 5
    LMHom   LMHom   LMHom   
   LMHom    |
97 | 1, 2, 6, 7 | mendplusg 36123 |
. . . . 5
     LMHom     LMHom                            |
98 | 79, 96, 97 | syl2anc 673 |
. . . 4
    LMHom   LMHom   LMHom   
                         |
99 | 1, 2, 71 | mendmulr 36125 |
. . . . . 6
   LMHom   LMHom  
            |
100 | 12, 15, 99 | syl2anc 673 |
. . . . 5
    LMHom   LMHom   LMHom   
            |
101 | 77, 100 | oveq12d 6326 |
. . . 4
    LMHom   LMHom   LMHom   
                                    |
102 | | lmghm 18332 |
. . . . . 6
  LMHom 

   |
103 | | ghmmhm 16971 |
. . . . . 6
  

MndHom    |
104 | 12, 102, 103 | 3syl 18 |
. . . . 5
    LMHom   LMHom   LMHom   

MndHom    |
105 | 31, 6, 6 | mhmvlin 19499 |
. . . . 5
   MndHom      
    
                                   |
106 | 104, 40, 44, 105 | syl3anc 1292 |
. . . 4
    LMHom   LMHom   LMHom   
                        |
107 | 98, 101, 106 | 3eqtr4d 2515 |
. . 3
    LMHom   LMHom   LMHom   
                                   |
108 | 93, 94, 107 | 3eqtr4d 2515 |
. 2
    LMHom   LMHom   LMHom   
                                        |
109 | 1, 2, 71 | mendmulr 36125 |
. . . 4
           LMHom   LMHom                               |
110 | 14, 15, 109 | syl2anc 673 |
. . 3
    LMHom   LMHom   LMHom   
                            |
111 | 18 | oveq1d 6323 |
. . 3
    LMHom   LMHom   LMHom   
                                 |
112 | 1, 2, 6, 7 | mendplusg 36123 |
. . . . 5
     LMHom     LMHom                            |
113 | 96, 87, 112 | syl2anc 673 |
. . . 4
    LMHom   LMHom   LMHom   
                         |
114 | 100, 84 | oveq12d 6326 |
. . . 4
    LMHom   LMHom   LMHom   
                                    |
115 | | ffn 5739 |
. . . . . 6
            
      |
116 | 12, 32, 115 | 3syl 18 |
. . . . 5
    LMHom   LMHom   LMHom   
      |
117 | | ffn 5739 |
. . . . . 6
            
      |
118 | 13, 37, 117 | 3syl 18 |
. . . . 5
    LMHom   LMHom   LMHom   
      |
119 | 34 | a1i 11 |
. . . . 5
    LMHom   LMHom   LMHom   
      |
120 | | inidm 3632 |
. . . . 5
               |
121 | 116, 118,
42, 119, 119, 119, 120 | ofco 6570 |
. . . 4
    LMHom   LMHom   LMHom   
                        |
122 | 113, 114,
121 | 3eqtr4d 2515 |
. . 3
    LMHom   LMHom   LMHom   
                                   |
123 | 110, 111,
122 | 3eqtr4d 2515 |
. 2
    LMHom   LMHom   LMHom   
                                        |
124 | 31 | idlmhm 18342 |
. 2

      LMHom    |
125 | 1, 2, 71 | mendmulr 36125 |
. . . 4
        LMHom 

LMHom                
        |
126 | 124, 125 | sylan 479 |
. . 3
   LMHom  
             
        |
127 | 32 | adantl 473 |
. . . 4
   LMHom  
              |
128 | | fcoi2 5770 |
. . . 4
            
         |
129 | 127, 128 | syl 17 |
. . 3
   LMHom  
         |
130 | 126, 129 | eqtrd 2505 |
. 2
   LMHom  
               |
131 | | id 22 |
. . . 4
  LMHom 

LMHom    |
132 | 1, 2, 71 | mendmulr 36125 |
. . . 4
   LMHom        LMHom                         |
133 | 131, 124,
132 | syl2anr 486 |
. . 3
   LMHom  
                      |
134 | | fcoi1 5769 |
. . . 4
            

        |
135 | 127, 134 | syl 17 |
. . 3
   LMHom  

        |
136 | 133, 135 | eqtrd 2505 |
. 2
   LMHom  
               |
137 | 3, 4, 5, 70, 75, 91, 108, 123, 124, 130, 136 | isringd 17893 |
1

  |