Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. 2
|
2 | | eqid 2622 |
. 2
|
3 | | eqid 2622 |
. 2
|
4 | | eqid 2622 |
. 2
Scalar Scalar |
5 | | eqid 2622 |
. 2
Scalar Scalar |
6 | | eqid 2622 |
. 2
Scalar Scalar |
7 | | lmhmlmod1 19033 |
. . 3
LMHom
|
8 | 7 | adantl 482 |
. 2
LMHom LMHom
|
9 | | lmhmlmod2 19032 |
. . 3
LMHom
|
10 | 9 | adantr 481 |
. 2
LMHom LMHom
|
11 | | eqid 2622 |
. . . 4
Scalar Scalar |
12 | 11, 5 | lmhmsca 19030 |
. . 3
LMHom
Scalar Scalar |
13 | 4, 11 | lmhmsca 19030 |
. . 3
LMHom
Scalar Scalar |
14 | 12, 13 | sylan9eq 2676 |
. 2
LMHom LMHom
Scalar Scalar |
15 | | lmghm 19031 |
. . 3
LMHom
|
16 | | lmghm 19031 |
. . 3
LMHom
|
17 | | ghmco 17680 |
. . 3
|
18 | 15, 16, 17 | syl2an 494 |
. 2
LMHom LMHom
|
19 | | simplr 792 |
. . . . . 6
LMHom
LMHom Scalar
LMHom |
20 | | simprl 794 |
. . . . . 6
LMHom
LMHom Scalar
Scalar |
21 | | simprr 796 |
. . . . . 6
LMHom
LMHom Scalar
|
22 | | eqid 2622 |
. . . . . . 7
|
23 | 4, 6, 1, 2, 22 | lmhmlin 19035 |
. . . . . 6
LMHom Scalar
|
24 | 19, 20, 21, 23 | syl3anc 1326 |
. . . . 5
LMHom
LMHom Scalar
|
25 | 24 | fveq2d 6195 |
. . . 4
LMHom
LMHom Scalar
|
26 | | simpll 790 |
. . . . 5
LMHom
LMHom Scalar
LMHom |
27 | 13 | fveq2d 6195 |
. . . . . . 7
LMHom
Scalar Scalar |
28 | 27 | ad2antlr 763 |
. . . . . 6
LMHom
LMHom Scalar
Scalar Scalar |
29 | 20, 28 | eleqtrrd 2704 |
. . . . 5
LMHom
LMHom Scalar
Scalar |
30 | | eqid 2622 |
. . . . . . . . 9
|
31 | 1, 30 | lmhmf 19034 |
. . . . . . . 8
LMHom
|
32 | 31 | adantl 482 |
. . . . . . 7
LMHom LMHom
|
33 | 32 | ffvelrnda 6359 |
. . . . . 6
LMHom
LMHom |
34 | 33 | adantrl 752 |
. . . . 5
LMHom
LMHom Scalar
|
35 | | eqid 2622 |
. . . . . 6
Scalar Scalar |
36 | 11, 35, 30, 22, 3 | lmhmlin 19035 |
. . . . 5
LMHom Scalar |
37 | 26, 29, 34, 36 | syl3anc 1326 |
. . . 4
LMHom
LMHom Scalar
|
38 | 25, 37 | eqtrd 2656 |
. . 3
LMHom
LMHom Scalar
|
39 | | ffn 6045 |
. . . . . 6
|
40 | 32, 39 | syl 17 |
. . . . 5
LMHom LMHom
|
41 | 40 | adantr 481 |
. . . 4
LMHom
LMHom Scalar
|
42 | 7 | ad2antlr 763 |
. . . . 5
LMHom
LMHom Scalar
|
43 | 1, 4, 2, 6 | lmodvscl 18880 |
. . . . 5
Scalar
|
44 | 42, 20, 21, 43 | syl3anc 1326 |
. . . 4
LMHom
LMHom Scalar
|
45 | | fvco2 6273 |
. . . 4
|
46 | 41, 44, 45 | syl2anc 693 |
. . 3
LMHom
LMHom Scalar
|
47 | | fvco2 6273 |
. . . . 5
|
48 | 41, 21, 47 | syl2anc 693 |
. . . 4
LMHom
LMHom Scalar
|
49 | 48 | oveq2d 6666 |
. . 3
LMHom
LMHom Scalar
|
50 | 38, 46, 49 | 3eqtr4d 2666 |
. 2
LMHom
LMHom Scalar
|
51 | 1, 2, 3, 4, 5, 6, 8, 10, 14, 18, 50 | islmhmd 19039 |
1
LMHom LMHom
LMHom |