Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lmhmsca | Structured version Visualization version GIF version |
Description: A homomorphism of left modules constrains both modules to the same ring of scalars. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
Ref | Expression |
---|---|
lmhmlem.k | ⊢ 𝐾 = (Scalar‘𝑆) |
lmhmlem.l | ⊢ 𝐿 = (Scalar‘𝑇) |
Ref | Expression |
---|---|
lmhmsca | ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐿 = 𝐾) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmhmlem.k | . . 3 ⊢ 𝐾 = (Scalar‘𝑆) | |
2 | lmhmlem.l | . . 3 ⊢ 𝐿 = (Scalar‘𝑇) | |
3 | 1, 2 | lmhmlem 19784 | . 2 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾))) |
4 | 3 | simprrd 772 | 1 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐿 = 𝐾) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ‘cfv 6341 (class class class)co 7142 Scalarcsca 16551 GrpHom cghm 18338 LModclmod 19617 LMHom clmhm 19774 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5189 ax-nul 5196 ax-pow 5252 ax-pr 5316 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3488 df-sbc 3764 df-dif 3927 df-un 3929 df-in 3931 df-ss 3940 df-nul 4280 df-if 4454 df-sn 4554 df-pr 4556 df-op 4560 df-uni 4825 df-br 5053 df-opab 5115 df-id 5446 df-xp 5547 df-rel 5548 df-cnv 5549 df-co 5550 df-dm 5551 df-iota 6300 df-fun 6343 df-fv 6349 df-ov 7145 df-oprab 7146 df-mpo 7147 df-lmhm 19777 |
This theorem is referenced by: islmhm2 19793 lmhmco 19798 lmhmplusg 19799 lmhmvsca 19800 lmhmf1o 19801 lmhmima 19802 lmhmpreima 19803 reslmhm 19807 reslmhm2 19808 reslmhm2b 19809 lindfmm 20954 lmhmclm 23674 nmoleub2lem3 23702 nmoleub3 23706 lmhmlvec2 31027 lmhmlvec 39223 |
Copyright terms: Public domain | W3C validator |