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
|- ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) -> ( F o. G ) e. ( M LMHom O ) )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( Base ` M ) = ( Base ` M )
2 eqid
 |-  ( .s ` M ) = ( .s ` M )
3 eqid
 |-  ( .s ` O ) = ( .s ` O )
4 eqid
 |-  ( Scalar ` M ) = ( Scalar ` M )
5 eqid
 |-  ( Scalar ` O ) = ( Scalar ` O )
6 eqid
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
7 lmhmlmod1
 |-  ( G e. ( M LMHom N ) -> M e. LMod )
8 7 adantl
 |-  ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) -> M e. LMod )
9 lmhmlmod2
 |-  ( F e. ( N LMHom O ) -> O e. LMod )
10 9 adantr
 |-  ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) -> O e. LMod )
11 eqid
 |-  ( Scalar ` N ) = ( Scalar ` N )
12 11 5 lmhmsca
 |-  ( F e. ( N LMHom O ) -> ( Scalar ` O ) = ( Scalar ` N ) )
13 4 11 lmhmsca
 |-  ( G e. ( M LMHom N ) -> ( Scalar ` N ) = ( Scalar ` M ) )
14 12 13 sylan9eq
 |-  ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) -> ( Scalar ` O ) = ( Scalar ` M ) )
15 lmghm
 |-  ( F e. ( N LMHom O ) -> F e. ( N GrpHom O ) )
16 lmghm
 |-  ( G e. ( M LMHom N ) -> G e. ( M GrpHom N ) )
17 ghmco
 |-  ( ( F e. ( N GrpHom O ) /\ G e. ( M GrpHom N ) ) -> ( F o. G ) e. ( M GrpHom O ) )
18 15 16 17 syl2an
 |-  ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) -> ( F o. G ) e. ( M GrpHom O ) )
19 simplr
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> G e. ( M LMHom N ) )
20 simprl
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> x e. ( Base ` ( Scalar ` M ) ) )
21 simprr
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> y e. ( Base ` M ) )
22 eqid
 |-  ( .s ` N ) = ( .s ` N )
23 4 6 1 2 22 lmhmlin
 |-  ( ( G e. ( M LMHom N ) /\ x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) -> ( G ` ( x ( .s ` M ) y ) ) = ( x ( .s ` N ) ( G ` y ) ) )
24 19 20 21 23 syl3anc
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( G ` ( x ( .s ` M ) y ) ) = ( x ( .s ` N ) ( G ` y ) ) )
25 24 fveq2d
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( F ` ( G ` ( x ( .s ` M ) y ) ) ) = ( F ` ( x ( .s ` N ) ( G ` y ) ) ) )
26 simpll
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> F e. ( N LMHom O ) )
27 13 fveq2d
 |-  ( G e. ( M LMHom N ) -> ( Base ` ( Scalar ` N ) ) = ( Base ` ( Scalar ` M ) ) )
28 27 ad2antlr
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( Base ` ( Scalar ` N ) ) = ( Base ` ( Scalar ` M ) ) )
29 20 28 eleqtrrd
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> x e. ( Base ` ( Scalar ` N ) ) )
30 eqid
 |-  ( Base ` N ) = ( Base ` N )
31 1 30 lmhmf
 |-  ( G e. ( M LMHom N ) -> G : ( Base ` M ) --> ( Base ` N ) )
32 31 adantl
 |-  ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) -> G : ( Base ` M ) --> ( Base ` N ) )
33 32 ffvelrnda
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ y e. ( Base ` M ) ) -> ( G ` y ) e. ( Base ` N ) )
34 33 adantrl
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( G ` y ) e. ( Base ` N ) )
35 eqid
 |-  ( Base ` ( Scalar ` N ) ) = ( Base ` ( Scalar ` N ) )
36 11 35 30 22 3 lmhmlin
 |-  ( ( F e. ( N LMHom O ) /\ x e. ( Base ` ( Scalar ` N ) ) /\ ( G ` y ) e. ( Base ` N ) ) -> ( F ` ( x ( .s ` N ) ( G ` y ) ) ) = ( x ( .s ` O ) ( F ` ( G ` y ) ) ) )
37 26 29 34 36 syl3anc
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( F ` ( x ( .s ` N ) ( G ` y ) ) ) = ( x ( .s ` O ) ( F ` ( G ` y ) ) ) )
38 25 37 eqtrd
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( F ` ( G ` ( x ( .s ` M ) y ) ) ) = ( x ( .s ` O ) ( F ` ( G ` y ) ) ) )
39 32 ffnd
 |-  ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) -> G Fn ( Base ` M ) )
40 7 ad2antlr
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> M e. LMod )
41 1 4 2 6 lmodvscl
 |-  ( ( M e. LMod /\ x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) -> ( x ( .s ` M ) y ) e. ( Base ` M ) )
42 40 20 21 41 syl3anc
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( x ( .s ` M ) y ) e. ( Base ` M ) )
43 fvco2
 |-  ( ( G Fn ( Base ` M ) /\ ( x ( .s ` M ) y ) e. ( Base ` M ) ) -> ( ( F o. G ) ` ( x ( .s ` M ) y ) ) = ( F ` ( G ` ( x ( .s ` M ) y ) ) ) )
44 39 42 43 syl2an2r
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( ( F o. G ) ` ( x ( .s ` M ) y ) ) = ( F ` ( G ` ( x ( .s ` M ) y ) ) ) )
45 fvco2
 |-  ( ( G Fn ( Base ` M ) /\ y e. ( Base ` M ) ) -> ( ( F o. G ) ` y ) = ( F ` ( G ` y ) ) )
46 39 21 45 syl2an2r
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( ( F o. G ) ` y ) = ( F ` ( G ` y ) ) )
47 46 oveq2d
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( x ( .s ` O ) ( ( F o. G ) ` y ) ) = ( x ( .s ` O ) ( F ` ( G ` y ) ) ) )
48 38 44 47 3eqtr4d
 |-  ( ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( ( F o. G ) ` ( x ( .s ` M ) y ) ) = ( x ( .s ` O ) ( ( F o. G ) ` y ) ) )
49 1 2 3 4 5 6 8 10 14 18 48 islmhmd
 |-  ( ( F e. ( N LMHom O ) /\ G e. ( M LMHom N ) ) -> ( F o. G ) e. ( M LMHom O ) )