Metamath Proof Explorer


Theorem islmhmd

Description: Deduction for a module homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015)

Ref Expression
Hypotheses islmhmd.x โŠข ๐‘‹ = ( Base โ€˜ ๐‘† )
islmhmd.a โŠข ยท = ( ยท๐‘  โ€˜ ๐‘† )
islmhmd.b โŠข ร— = ( ยท๐‘  โ€˜ ๐‘‡ )
islmhmd.k โŠข ๐พ = ( Scalar โ€˜ ๐‘† )
islmhmd.j โŠข ๐ฝ = ( Scalar โ€˜ ๐‘‡ )
islmhmd.n โŠข ๐‘ = ( Base โ€˜ ๐พ )
islmhmd.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ LMod )
islmhmd.t โŠข ( ๐œ‘ โ†’ ๐‘‡ โˆˆ LMod )
islmhmd.c โŠข ( ๐œ‘ โ†’ ๐ฝ = ๐พ )
islmhmd.f โŠข ( ๐œ‘ โ†’ ๐น โˆˆ ( ๐‘† GrpHom ๐‘‡ ) )
islmhmd.l โŠข ( ( ๐œ‘ โˆง ( ๐‘ฅ โˆˆ ๐‘ โˆง ๐‘ฆ โˆˆ ๐‘‹ ) ) โ†’ ( ๐น โ€˜ ( ๐‘ฅ ยท ๐‘ฆ ) ) = ( ๐‘ฅ ร— ( ๐น โ€˜ ๐‘ฆ ) ) )
Assertion islmhmd ( ๐œ‘ โ†’ ๐น โˆˆ ( ๐‘† LMHom ๐‘‡ ) )

Proof

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 ๐‘‡ ) )