Step |
Hyp |
Ref |
Expression |
1 |
|
lmhmlin.k |
โข ๐พ = ( Scalar โ ๐ ) |
2 |
|
lmhmlin.b |
โข ๐ต = ( Base โ ๐พ ) |
3 |
|
lmhmlin.e |
โข ๐ธ = ( Base โ ๐ ) |
4 |
|
lmhmlin.m |
โข ยท = ( ยท๐ โ ๐ ) |
5 |
|
lmhmlin.n |
โข ร = ( ยท๐ โ ๐ ) |
6 |
|
eqid |
โข ( Scalar โ ๐ ) = ( Scalar โ ๐ ) |
7 |
1 6 2 3 4 5
|
islmhm |
โข ( ๐น โ ( ๐ LMHom ๐ ) โ ( ( ๐ โ LMod โง ๐ โ LMod ) โง ( ๐น โ ( ๐ GrpHom ๐ ) โง ( Scalar โ ๐ ) = ๐พ โง โ ๐ โ ๐ต โ ๐ โ ๐ธ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐ ร ( ๐น โ ๐ ) ) ) ) ) |
8 |
7
|
simprbi |
โข ( ๐น โ ( ๐ LMHom ๐ ) โ ( ๐น โ ( ๐ GrpHom ๐ ) โง ( Scalar โ ๐ ) = ๐พ โง โ ๐ โ ๐ต โ ๐ โ ๐ธ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐ ร ( ๐น โ ๐ ) ) ) ) |
9 |
8
|
simp3d |
โข ( ๐น โ ( ๐ LMHom ๐ ) โ โ ๐ โ ๐ต โ ๐ โ ๐ธ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐ ร ( ๐น โ ๐ ) ) ) |
10 |
|
fvoveq1 |
โข ( ๐ = ๐ โ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐น โ ( ๐ ยท ๐ ) ) ) |
11 |
|
oveq1 |
โข ( ๐ = ๐ โ ( ๐ ร ( ๐น โ ๐ ) ) = ( ๐ ร ( ๐น โ ๐ ) ) ) |
12 |
10 11
|
eqeq12d |
โข ( ๐ = ๐ โ ( ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐ ร ( ๐น โ ๐ ) ) โ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐ ร ( ๐น โ ๐ ) ) ) ) |
13 |
|
oveq2 |
โข ( ๐ = ๐ โ ( ๐ ยท ๐ ) = ( ๐ ยท ๐ ) ) |
14 |
13
|
fveq2d |
โข ( ๐ = ๐ โ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐น โ ( ๐ ยท ๐ ) ) ) |
15 |
|
fveq2 |
โข ( ๐ = ๐ โ ( ๐น โ ๐ ) = ( ๐น โ ๐ ) ) |
16 |
15
|
oveq2d |
โข ( ๐ = ๐ โ ( ๐ ร ( ๐น โ ๐ ) ) = ( ๐ ร ( ๐น โ ๐ ) ) ) |
17 |
14 16
|
eqeq12d |
โข ( ๐ = ๐ โ ( ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐ ร ( ๐น โ ๐ ) ) โ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐ ร ( ๐น โ ๐ ) ) ) ) |
18 |
12 17
|
rspc2v |
โข ( ( ๐ โ ๐ต โง ๐ โ ๐ธ ) โ ( โ ๐ โ ๐ต โ ๐ โ ๐ธ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐ ร ( ๐น โ ๐ ) ) โ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐ ร ( ๐น โ ๐ ) ) ) ) |
19 |
9 18
|
syl5com |
โข ( ๐น โ ( ๐ LMHom ๐ ) โ ( ( ๐ โ ๐ต โง ๐ โ ๐ธ ) โ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐ ร ( ๐น โ ๐ ) ) ) ) |
20 |
19
|
3impib |
โข ( ( ๐น โ ( ๐ LMHom ๐ ) โง ๐ โ ๐ต โง ๐ โ ๐ธ ) โ ( ๐น โ ( ๐ ยท ๐ ) ) = ( ๐ ร ( ๐น โ ๐ ) ) ) |