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 ) )