Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lmghm | Structured version Visualization version GIF version |
Description: A homomorphism of left modules is a homomorphism of groups. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
Ref | Expression |
---|---|
lmghm | ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2739 | . . 3 ⊢ (Scalar‘𝑆) = (Scalar‘𝑆) | |
2 | eqid 2739 | . . 3 ⊢ (Scalar‘𝑇) = (Scalar‘𝑇) | |
3 | 1, 2 | lmhmlem 20272 | . 2 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (Scalar‘𝑇) = (Scalar‘𝑆)))) |
4 | 3 | simprld 768 | 1 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2109 ‘cfv 6430 (class class class)co 7268 Scalarcsca 16946 GrpHom cghm 18812 LModclmod 20104 LMHom clmhm 20262 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-8 2111 ax-9 2119 ax-10 2140 ax-11 2157 ax-12 2174 ax-ext 2710 ax-sep 5226 ax-nul 5233 ax-pr 5355 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1544 df-fal 1554 df-ex 1786 df-nf 1790 df-sb 2071 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-ral 3070 df-rex 3071 df-rab 3074 df-v 3432 df-sbc 3720 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-nul 4262 df-if 4465 df-sn 4567 df-pr 4569 df-op 4573 df-uni 4845 df-br 5079 df-opab 5141 df-id 5488 df-xp 5594 df-rel 5595 df-cnv 5596 df-co 5597 df-dm 5598 df-iota 6388 df-fun 6432 df-fv 6438 df-ov 7271 df-oprab 7272 df-mpo 7273 df-lmhm 20265 |
This theorem is referenced by: lmhmf 20277 islmhm2 20281 lmhmco 20286 lmhmplusg 20287 lmhmvsca 20288 lmhmf1o 20289 lmhmima 20290 lmhmpreima 20291 reslmhm 20295 reslmhm2 20296 reslmhm2b 20297 lmhmeql 20298 lmimgim 20308 ip0l 20822 ipdir 20825 islindf5 21027 isnmhm2 23897 nmoleub2lem 24258 nmoleub2lem2 24260 nmhmcn 24264 dimkerim 31687 kercvrlsm 40888 pwssplit4 40894 mendring 40997 |
Copyright terms: Public domain | W3C validator |