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