Metamath Proof Explorer


Theorem lmhmco

Description: The composition of two module-linear functions is module-linear. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Assertion lmhmco FNLMHomOGMLMHomNFGMLMHomO

Proof

Step Hyp Ref Expression
1 eqid BaseM=BaseM
2 eqid M=M
3 eqid O=O
4 eqid ScalarM=ScalarM
5 eqid ScalarO=ScalarO
6 eqid BaseScalarM=BaseScalarM
7 lmhmlmod1 GMLMHomNMLMod
8 7 adantl FNLMHomOGMLMHomNMLMod
9 lmhmlmod2 FNLMHomOOLMod
10 9 adantr FNLMHomOGMLMHomNOLMod
11 eqid ScalarN=ScalarN
12 11 5 lmhmsca FNLMHomOScalarO=ScalarN
13 4 11 lmhmsca GMLMHomNScalarN=ScalarM
14 12 13 sylan9eq FNLMHomOGMLMHomNScalarO=ScalarM
15 lmghm FNLMHomOFNGrpHomO
16 lmghm GMLMHomNGMGrpHomN
17 ghmco FNGrpHomOGMGrpHomNFGMGrpHomO
18 15 16 17 syl2an FNLMHomOGMLMHomNFGMGrpHomO
19 simplr FNLMHomOGMLMHomNxBaseScalarMyBaseMGMLMHomN
20 simprl FNLMHomOGMLMHomNxBaseScalarMyBaseMxBaseScalarM
21 simprr FNLMHomOGMLMHomNxBaseScalarMyBaseMyBaseM
22 eqid N=N
23 4 6 1 2 22 lmhmlin GMLMHomNxBaseScalarMyBaseMGxMy=xNGy
24 19 20 21 23 syl3anc FNLMHomOGMLMHomNxBaseScalarMyBaseMGxMy=xNGy
25 24 fveq2d FNLMHomOGMLMHomNxBaseScalarMyBaseMFGxMy=FxNGy
26 simpll FNLMHomOGMLMHomNxBaseScalarMyBaseMFNLMHomO
27 13 fveq2d GMLMHomNBaseScalarN=BaseScalarM
28 27 ad2antlr FNLMHomOGMLMHomNxBaseScalarMyBaseMBaseScalarN=BaseScalarM
29 20 28 eleqtrrd FNLMHomOGMLMHomNxBaseScalarMyBaseMxBaseScalarN
30 eqid BaseN=BaseN
31 1 30 lmhmf GMLMHomNG:BaseMBaseN
32 31 adantl FNLMHomOGMLMHomNG:BaseMBaseN
33 32 ffvelcdmda FNLMHomOGMLMHomNyBaseMGyBaseN
34 33 adantrl FNLMHomOGMLMHomNxBaseScalarMyBaseMGyBaseN
35 eqid BaseScalarN=BaseScalarN
36 11 35 30 22 3 lmhmlin FNLMHomOxBaseScalarNGyBaseNFxNGy=xOFGy
37 26 29 34 36 syl3anc FNLMHomOGMLMHomNxBaseScalarMyBaseMFxNGy=xOFGy
38 25 37 eqtrd FNLMHomOGMLMHomNxBaseScalarMyBaseMFGxMy=xOFGy
39 32 ffnd FNLMHomOGMLMHomNGFnBaseM
40 7 ad2antlr FNLMHomOGMLMHomNxBaseScalarMyBaseMMLMod
41 1 4 2 6 lmodvscl MLModxBaseScalarMyBaseMxMyBaseM
42 40 20 21 41 syl3anc FNLMHomOGMLMHomNxBaseScalarMyBaseMxMyBaseM
43 fvco2 GFnBaseMxMyBaseMFGxMy=FGxMy
44 39 42 43 syl2an2r FNLMHomOGMLMHomNxBaseScalarMyBaseMFGxMy=FGxMy
45 fvco2 GFnBaseMyBaseMFGy=FGy
46 39 21 45 syl2an2r FNLMHomOGMLMHomNxBaseScalarMyBaseMFGy=FGy
47 46 oveq2d FNLMHomOGMLMHomNxBaseScalarMyBaseMxOFGy=xOFGy
48 38 44 47 3eqtr4d FNLMHomOGMLMHomNxBaseScalarMyBaseMFGxMy=xOFGy
49 1 2 3 4 5 6 8 10 14 18 48 islmhmd FNLMHomOGMLMHomNFGMLMHomO