Step | Hyp | Ref
| Expression |
1 | | mendassa.a |
. . . 4
MEndo |
2 | 1 | mendbas 37754 |
. . 3
LMHom |
3 | 2 | a1i 11 |
. 2
LMHom |
4 | | eqidd 2623 |
. 2
|
5 | | mendassa.s |
. . . 4
Scalar |
6 | 1, 5 | mendsca 37759 |
. . 3
Scalar |
7 | 6 | a1i 11 |
. 2
Scalar |
8 | | eqidd 2623 |
. 2
|
9 | | eqidd 2623 |
. 2
|
10 | | eqidd 2623 |
. 2
|
11 | | eqidd 2623 |
. 2
|
12 | | eqidd 2623 |
. 2
|
13 | | crngring 18558 |
. . 3
|
14 | 13 | adantl 482 |
. 2
|
15 | 1 | mendring 37762 |
. . . 4
|
16 | 15 | adantr 481 |
. . 3
|
17 | | ringgrp 18552 |
. . 3
|
18 | 16, 17 | syl 17 |
. 2
|
19 | | eqid 2622 |
. . . . 5
|
20 | | eqid 2622 |
. . . . 5
|
21 | | eqid 2622 |
. . . . 5
|
22 | | eqid 2622 |
. . . . 5
|
23 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 37761 |
. . . 4
LMHom
|
24 | 23 | 3adant1 1079 |
. . 3
LMHom
|
25 | 21, 19, 5, 20 | lmhmvsca 19045 |
. . . 4
LMHom LMHom |
26 | 25 | 3adant1l 1318 |
. . 3
LMHom
LMHom |
27 | 24, 26 | eqeltrd 2701 |
. 2
LMHom
LMHom |
28 | | simpr2 1068 |
. . . . 5
LMHom LMHom LMHom |
29 | | simpr3 1069 |
. . . . 5
LMHom LMHom LMHom |
30 | | eqid 2622 |
. . . . . 6
|
31 | | eqid 2622 |
. . . . . 6
|
32 | 1, 2, 30, 31 | mendplusg 37756 |
. . . . 5
LMHom LMHom
|
33 | 28, 29, 32 | syl2anc 693 |
. . . 4
LMHom LMHom |
34 | 33 | oveq2d 6666 |
. . 3
LMHom LMHom |
35 | | simpr1 1067 |
. . . 4
LMHom LMHom |
36 | 18 | adantr 481 |
. . . . 5
LMHom LMHom |
37 | 2, 31 | grpcl 17430 |
. . . . 5
LMHom LMHom
LMHom |
38 | 36, 28, 29, 37 | syl3anc 1326 |
. . . 4
LMHom LMHom LMHom |
39 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 37761 |
. . . 4
LMHom
|
40 | 35, 38, 39 | syl2anc 693 |
. . 3
LMHom LMHom |
41 | 35, 28, 23 | syl2anc 693 |
. . . . 5
LMHom LMHom |
42 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 37761 |
. . . . . 6
LMHom
|
43 | 35, 29, 42 | syl2anc 693 |
. . . . 5
LMHom LMHom |
44 | 41, 43 | oveq12d 6668 |
. . . 4
LMHom LMHom |
45 | 27 | 3adant3r3 1276 |
. . . . 5
LMHom LMHom LMHom |
46 | | eleq1 2689 |
. . . . . . . . 9
LMHom
LMHom |
47 | 46 | 3anbi3d 1405 |
. . . . . . . 8
LMHom
LMHom |
48 | | oveq2 6658 |
. . . . . . . . 9
|
49 | 48 | eleq1d 2686 |
. . . . . . . 8
LMHom
LMHom |
50 | 47, 49 | imbi12d 334 |
. . . . . . 7
LMHom LMHom
LMHom LMHom |
51 | 50, 27 | chvarv 2263 |
. . . . . 6
LMHom
LMHom |
52 | 51 | 3adant3r2 1275 |
. . . . 5
LMHom LMHom LMHom |
53 | 1, 2, 30, 31 | mendplusg 37756 |
. . . . 5
LMHom LMHom |
54 | 45, 52, 53 | syl2anc 693 |
. . . 4
LMHom LMHom |
55 | | fvexd 6203 |
. . . . 5
LMHom LMHom |
56 | | fconst6g 6094 |
. . . . . 6
|
57 | 35, 56 | syl 17 |
. . . . 5
LMHom LMHom |
58 | 21, 21 | lmhmf 19034 |
. . . . . 6
LMHom
|
59 | 28, 58 | syl 17 |
. . . . 5
LMHom LMHom |
60 | 21, 21 | lmhmf 19034 |
. . . . . 6
LMHom
|
61 | 29, 60 | syl 17 |
. . . . 5
LMHom LMHom |
62 | | simpll 790 |
. . . . . 6
LMHom LMHom |
63 | 21, 30, 5, 19, 20 | lmodvsdi 18886 |
. . . . . 6
|
64 | 62, 63 | sylan 488 |
. . . . 5
LMHom
LMHom
|
65 | 55, 57, 59, 61, 64 | caofdi 6933 |
. . . 4
LMHom LMHom |
66 | 44, 54, 65 | 3eqtr4d 2666 |
. . 3
LMHom LMHom |
67 | 34, 40, 66 | 3eqtr4d 2666 |
. 2
LMHom LMHom |
68 | | fvexd 6203 |
. . . 4
LMHom |
69 | | simpr3 1069 |
. . . . 5
LMHom LMHom |
70 | 69, 60 | syl 17 |
. . . 4
LMHom |
71 | | simpr1 1067 |
. . . . 5
LMHom |
72 | 71, 56 | syl 17 |
. . . 4
LMHom |
73 | | simpr2 1068 |
. . . . 5
LMHom |
74 | | fconst6g 6094 |
. . . . 5
|
75 | 73, 74 | syl 17 |
. . . 4
LMHom |
76 | | simpll 790 |
. . . . 5
LMHom |
77 | | eqid 2622 |
. . . . . 6
|
78 | 21, 30, 5, 19, 20, 77 | lmodvsdir 18887 |
. . . . 5
|
79 | 76, 78 | sylan 488 |
. . . 4
LMHom
|
80 | 68, 70, 72, 75, 79 | caofdir 6934 |
. . 3
LMHom |
81 | 14 | adantr 481 |
. . . . . 6
LMHom |
82 | 20, 77 | ringacl 18578 |
. . . . . 6
|
83 | 81, 71, 73, 82 | syl3anc 1326 |
. . . . 5
LMHom |
84 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 37761 |
. . . . 5
LMHom |
85 | 83, 69, 84 | syl2anc 693 |
. . . 4
LMHom |
86 | 68, 71, 73 | ofc12 6922 |
. . . . 5
LMHom |
87 | 86 | oveq1d 6665 |
. . . 4
LMHom |
88 | 85, 87 | eqtr4d 2659 |
. . 3
LMHom |
89 | 51 | 3adant3r2 1275 |
. . . . 5
LMHom LMHom |
90 | | eleq1 2689 |
. . . . . . . . 9
|
91 | 90 | 3anbi2d 1404 |
. . . . . . . 8
LMHom
LMHom |
92 | | oveq1 6657 |
. . . . . . . . 9
|
93 | 92 | eleq1d 2686 |
. . . . . . . 8
LMHom
LMHom |
94 | 91, 93 | imbi12d 334 |
. . . . . . 7
LMHom LMHom
LMHom LMHom |
95 | 94, 51 | chvarv 2263 |
. . . . . 6
LMHom
LMHom |
96 | 95 | 3adant3r1 1274 |
. . . . 5
LMHom LMHom |
97 | 1, 2, 30, 31 | mendplusg 37756 |
. . . . 5
LMHom LMHom |
98 | 89, 96, 97 | syl2anc 693 |
. . . 4
LMHom |
99 | 71, 69, 42 | syl2anc 693 |
. . . . 5
LMHom |
100 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 37761 |
. . . . . 6
LMHom
|
101 | 73, 69, 100 | syl2anc 693 |
. . . . 5
LMHom |
102 | 99, 101 | oveq12d 6668 |
. . . 4
LMHom |
103 | 98, 102 | eqtrd 2656 |
. . 3
LMHom |
104 | 80, 88, 103 | 3eqtr4d 2666 |
. 2
LMHom |
105 | | ovexd 6680 |
. . . 4
LMHom
|
106 | 70 | ffvelrnda 6359 |
. . . 4
LMHom
|
107 | | fconstmpt 5163 |
. . . . 5
|
108 | 107 | a1i 11 |
. . . 4
LMHom |
109 | 70 | feqmptd 6249 |
. . . 4
LMHom |
110 | 68, 105, 106, 108, 109 | offval2 6914 |
. . 3
LMHom |
111 | | eqid 2622 |
. . . . . 6
|
112 | 20, 111 | ringcl 18561 |
. . . . 5
|
113 | 81, 71, 73, 112 | syl3anc 1326 |
. . . 4
LMHom |
114 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 37761 |
. . . 4
LMHom
|
115 | 113, 69, 114 | syl2anc 693 |
. . 3
LMHom |
116 | 71 | adantr 481 |
. . . . 5
LMHom
|
117 | | ovexd 6680 |
. . . . 5
LMHom
|
118 | | fconstmpt 5163 |
. . . . . 6
|
119 | 118 | a1i 11 |
. . . . 5
LMHom |
120 | | simplr2 1104 |
. . . . . . 7
LMHom
|
121 | | fconstmpt 5163 |
. . . . . . . 8
|
122 | 121 | a1i 11 |
. . . . . . 7
LMHom |
123 | 68, 120, 106, 122, 109 | offval2 6914 |
. . . . . 6
LMHom |
124 | 101, 123 | eqtrd 2656 |
. . . . 5
LMHom |
125 | 68, 116, 117, 119, 124 | offval2 6914 |
. . . 4
LMHom |
126 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 37761 |
. . . . 5
LMHom |
127 | 71, 96, 126 | syl2anc 693 |
. . . 4
LMHom |
128 | 76 | adantr 481 |
. . . . . 6
LMHom
|
129 | 21, 5, 19, 20, 111 | lmodvsass 18888 |
. . . . . 6
|
130 | 128, 116,
120, 106, 129 | syl13anc 1328 |
. . . . 5
LMHom
|
131 | 130 | mpteq2dva 4744 |
. . . 4
LMHom |
132 | 125, 127,
131 | 3eqtr4d 2666 |
. . 3
LMHom |
133 | 110, 115,
132 | 3eqtr4d 2666 |
. 2
LMHom |
134 | 14 | adantr 481 |
. . . . 5
LMHom |
135 | | eqid 2622 |
. . . . . 6
|
136 | 20, 135 | ringidcl 18568 |
. . . . 5
|
137 | 134, 136 | syl 17 |
. . . 4
LMHom |
138 | 1, 19, 2, 5, 20, 21, 22 | mendvsca 37761 |
. . . 4
LMHom
|
139 | 137, 138 | sylancom 701 |
. . 3
LMHom |
140 | | fvexd 6203 |
. . . 4
LMHom |
141 | 21, 21 | lmhmf 19034 |
. . . . 5
LMHom
|
142 | 141 | adantl 482 |
. . . 4
LMHom |
143 | | simpll 790 |
. . . . 5
LMHom |
144 | 21, 5, 19, 135 | lmodvs1 18891 |
. . . . 5
|
145 | 143, 144 | sylan 488 |
. . . 4
LMHom
|
146 | 140, 142,
137, 145 | caofid0l 6925 |
. . 3
LMHom |
147 | 139, 146 | eqtrd 2656 |
. 2
LMHom |
148 | 3, 4, 7, 8, 9, 10,
11, 12, 14, 18, 27, 67, 104, 133, 147 | islmodd 18869 |
1
|