Theorem lmhmsca 20943

Description: A homomorphism of left modules constrains both modules to the same ring of scalars. (Contributed by Stefan O'Rear, 1-Jan-2015.)

Hypotheses

Ref	Expression
lmhmlem.k	⊢ 𝐾 = (Scalar‘𝑆)
lmhmlem.l	⊢ 𝐿 = (Scalar‘𝑇)

Assertion

Ref	Expression
lmhmsca	⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐿 = 𝐾)

Proof of Theorem lmhmsca

Step	Hyp	Ref	Expression
1		lmhmlem.k	. . 3 ⊢ 𝐾 = (Scalar‘𝑆)
2		lmhmlem.l	. . 3 ⊢ 𝐿 = (Scalar‘𝑇)
3	1, 2	lmhmlem 20942	. 2 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐿 = 𝐾)))
4	3	simprrd 773	1 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐿 = 𝐾)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ‘cfv 6513  (class class class)co 7389  Scalarcsca 17229   GrpHom cghm 19150  LModclmod 20772   LMHom clmhm 20932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pr 5389

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3756  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-iota 6466  df-fun 6515  df-fv 6521  df-ov 7392  df-oprab 7393  df-mpo 7394  df-lmhm 20935

This theorem is referenced by:  islmhm2  20951  lmhmco  20956  lmhmplusg  20957  lmhmvsca  20958  lmhmf1o  20959  lmhmima  20960  lmhmpreima  20961  reslmhm  20965  reslmhm2  20966  reslmhm2b  20967  lmhmlvec  21023  lindfmm  21742  lmhmclm  24993  nmoleub2lem3  25021  nmoleub3  25025  lmhmqusker  33394  lmhmlvec2  33621