Step |
Hyp |
Ref |
Expression |
1 |
|
islmhmd.x |
โข ๐ = ( Base โ ๐ ) |
2 |
|
islmhmd.a |
โข ยท = ( ยท๐ โ ๐ ) |
3 |
|
islmhmd.b |
โข ร = ( ยท๐ โ ๐ ) |
4 |
|
islmhmd.k |
โข ๐พ = ( Scalar โ ๐ ) |
5 |
|
islmhmd.j |
โข ๐ฝ = ( Scalar โ ๐ ) |
6 |
|
islmhmd.n |
โข ๐ = ( Base โ ๐พ ) |
7 |
|
islmhmd.s |
โข ( ๐ โ ๐ โ LMod ) |
8 |
|
islmhmd.t |
โข ( ๐ โ ๐ โ LMod ) |
9 |
|
islmhmd.c |
โข ( ๐ โ ๐ฝ = ๐พ ) |
10 |
|
islmhmd.f |
โข ( ๐ โ ๐น โ ( ๐ GrpHom ๐ ) ) |
11 |
|
islmhmd.l |
โข ( ( ๐ โง ( ๐ฅ โ ๐ โง ๐ฆ โ ๐ ) ) โ ( ๐น โ ( ๐ฅ ยท ๐ฆ ) ) = ( ๐ฅ ร ( ๐น โ ๐ฆ ) ) ) |
12 |
11
|
ralrimivva |
โข ( ๐ โ โ ๐ฅ โ ๐ โ ๐ฆ โ ๐ ( ๐น โ ( ๐ฅ ยท ๐ฆ ) ) = ( ๐ฅ ร ( ๐น โ ๐ฆ ) ) ) |
13 |
10 9 12
|
3jca |
โข ( ๐ โ ( ๐น โ ( ๐ GrpHom ๐ ) โง ๐ฝ = ๐พ โง โ ๐ฅ โ ๐ โ ๐ฆ โ ๐ ( ๐น โ ( ๐ฅ ยท ๐ฆ ) ) = ( ๐ฅ ร ( ๐น โ ๐ฆ ) ) ) ) |
14 |
4 5 6 1 2 3
|
islmhm |
โข ( ๐น โ ( ๐ LMHom ๐ ) โ ( ( ๐ โ LMod โง ๐ โ LMod ) โง ( ๐น โ ( ๐ GrpHom ๐ ) โง ๐ฝ = ๐พ โง โ ๐ฅ โ ๐ โ ๐ฆ โ ๐ ( ๐น โ ( ๐ฅ ยท ๐ฆ ) ) = ( ๐ฅ ร ( ๐น โ ๐ฆ ) ) ) ) ) |
15 |
7 8 13 14
|
syl21anbrc |
โข ( ๐ โ ๐น โ ( ๐ LMHom ๐ ) ) |