Description: The composition of two module-linear functions is module-linear. (Contributed by Stefan O'Rear, 4-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | lmhmco | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | eqid | |
|
3 | eqid | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | lmhmlmod1 | |
|
8 | 7 | adantl | |
9 | lmhmlmod2 | |
|
10 | 9 | adantr | |
11 | eqid | |
|
12 | 11 5 | lmhmsca | |
13 | 4 11 | lmhmsca | |
14 | 12 13 | sylan9eq | |
15 | lmghm | |
|
16 | lmghm | |
|
17 | ghmco | |
|
18 | 15 16 17 | syl2an | |
19 | simplr | |
|
20 | simprl | |
|
21 | simprr | |
|
22 | eqid | |
|
23 | 4 6 1 2 22 | lmhmlin | |
24 | 19 20 21 23 | syl3anc | |
25 | 24 | fveq2d | |
26 | simpll | |
|
27 | 13 | fveq2d | |
28 | 27 | ad2antlr | |
29 | 20 28 | eleqtrrd | |
30 | eqid | |
|
31 | 1 30 | lmhmf | |
32 | 31 | adantl | |
33 | 32 | ffvelcdmda | |
34 | 33 | adantrl | |
35 | eqid | |
|
36 | 11 35 30 22 3 | lmhmlin | |
37 | 26 29 34 36 | syl3anc | |
38 | 25 37 | eqtrd | |
39 | 32 | ffnd | |
40 | 7 | ad2antlr | |
41 | 1 4 2 6 | lmodvscl | |
42 | 40 20 21 41 | syl3anc | |
43 | fvco2 | |
|
44 | 39 42 43 | syl2an2r | |
45 | fvco2 | |
|
46 | 39 21 45 | syl2an2r | |
47 | 46 | oveq2d | |
48 | 38 44 47 | 3eqtr4d | |
49 | 1 2 3 4 5 6 8 10 14 18 48 | islmhmd | |