| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eqid |
⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 ) |
| 2 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 ) |
| 3 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑂 ) = ( ·𝑠 ‘ 𝑂 ) |
| 4 |
|
eqid |
⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 ) |
| 5 |
|
eqid |
⊢ ( Scalar ‘ 𝑂 ) = ( Scalar ‘ 𝑂 ) |
| 6 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) |
| 7 |
|
lmhmlmod1 |
⊢ ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) → 𝑀 ∈ LMod ) |
| 8 |
7
|
adantl |
⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝑀 ∈ LMod ) |
| 9 |
|
lmhmlmod2 |
⊢ ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) → 𝑂 ∈ LMod ) |
| 10 |
9
|
adantr |
⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝑂 ∈ LMod ) |
| 11 |
|
eqid |
⊢ ( Scalar ‘ 𝑁 ) = ( Scalar ‘ 𝑁 ) |
| 12 |
11 5
|
lmhmsca |
⊢ ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) → ( Scalar ‘ 𝑂 ) = ( Scalar ‘ 𝑁 ) ) |
| 13 |
4 11
|
lmhmsca |
⊢ ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) → ( Scalar ‘ 𝑁 ) = ( Scalar ‘ 𝑀 ) ) |
| 14 |
12 13
|
sylan9eq |
⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( Scalar ‘ 𝑂 ) = ( Scalar ‘ 𝑀 ) ) |
| 15 |
|
lmghm |
⊢ ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) → 𝐹 ∈ ( 𝑁 GrpHom 𝑂 ) ) |
| 16 |
|
lmghm |
⊢ ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) |
| 17 |
|
ghmco |
⊢ ( ( 𝐹 ∈ ( 𝑁 GrpHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 GrpHom 𝑁 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑀 GrpHom 𝑂 ) ) |
| 18 |
15 16 17
|
syl2an |
⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑀 GrpHom 𝑂 ) ) |
| 19 |
|
simplr |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) |
| 20 |
|
simprl |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) |
| 21 |
|
simprr |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑀 ) ) |
| 22 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑁 ) = ( ·𝑠 ‘ 𝑁 ) |
| 23 |
4 6 1 2 22
|
lmhmlin |
⊢ ( ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) ) |
| 24 |
19 20 21 23
|
syl3anc |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) ) |
| 25 |
24
|
fveq2d |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) ) ) |
| 26 |
|
simpll |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ) |
| 27 |
13
|
fveq2d |
⊢ ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) → ( Base ‘ ( Scalar ‘ 𝑁 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) |
| 28 |
27
|
ad2antlr |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( Base ‘ ( Scalar ‘ 𝑁 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) |
| 29 |
20 28
|
eleqtrrd |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑁 ) ) ) |
| 30 |
|
eqid |
⊢ ( Base ‘ 𝑁 ) = ( Base ‘ 𝑁 ) |
| 31 |
1 30
|
lmhmf |
⊢ ( 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) → 𝐺 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) ) |
| 32 |
31
|
adantl |
⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐺 : ( Base ‘ 𝑀 ) ⟶ ( Base ‘ 𝑁 ) ) |
| 33 |
32
|
ffvelrnda |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) ) |
| 34 |
33
|
adantrl |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) ) |
| 35 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝑁 ) ) = ( Base ‘ ( Scalar ‘ 𝑁 ) ) |
| 36 |
11 35 30 22 3
|
lmhmlin |
⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑁 ) ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ ( Base ‘ 𝑁 ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑂 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) |
| 37 |
26 29 34 36
|
syl3anc |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑁 ) ( 𝐺 ‘ 𝑦 ) ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑂 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) |
| 38 |
25 37
|
eqtrd |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑂 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) |
| 39 |
32
|
ffnd |
⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → 𝐺 Fn ( Base ‘ 𝑀 ) ) |
| 40 |
7
|
ad2antlr |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → 𝑀 ∈ LMod ) |
| 41 |
1 4 2 6
|
lmodvscl |
⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) |
| 42 |
40 20 21 41
|
syl3anc |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) |
| 43 |
|
fvco2 |
⊢ ( ( 𝐺 Fn ( Base ‘ 𝑀 ) ∧ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) ) |
| 44 |
39 42 43
|
syl2an2r |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) ) ) |
| 45 |
|
fvco2 |
⊢ ( ( 𝐺 Fn ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) |
| 46 |
39 21 45
|
syl2an2r |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) |
| 47 |
46
|
oveq2d |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑂 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑂 ) ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) |
| 48 |
38 44 47
|
3eqtr4d |
⊢ ( ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑂 ) ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) ) |
| 49 |
1 2 3 4 5 6 8 10 14 18 48
|
islmhmd |
⊢ ( ( 𝐹 ∈ ( 𝑁 LMHom 𝑂 ) ∧ 𝐺 ∈ ( 𝑀 LMHom 𝑁 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑀 LMHom 𝑂 ) ) |