Theorem lmhmlmod2 20377

Description: A homomorphism of left modules has a left module as codomain. (Contributed by Stefan O'Rear, 1-Jan-2015.)

Assertion

Ref	Expression
lmhmlmod2	⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod)

Proof of Theorem lmhmlmod2

Step	Hyp	Ref	Expression
1		eqid 2737	. . 3 ⊢ (Scalar‘𝑆) = (Scalar‘𝑆)
2		eqid 2737	. . 3 ⊢ (Scalar‘𝑇) = (Scalar‘𝑇)
3	1, 2	lmhmlem 20374	. 2 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (Scalar‘𝑇) = (Scalar‘𝑆))))
4	3	simplrd 767	1 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑇 ∈ LMod)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ∈ wcel 2105  ‘cfv 6466  (class class class)co 7317  Scalarcsca 17042   GrpHom cghm 18907  LModclmod 20206   LMHom clmhm 20364

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-sbc 3727  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-id 5507  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-iota 6418  df-fun 6468  df-fv 6474  df-ov 7320  df-oprab 7321  df-mpo 7322  df-lmhm 20367

This theorem is referenced by:  lmhmco  20388  lmhmplusg  20389  lmhmvsca  20390  lmhmf1o  20391  lmhmima  20392  lmhmpreima  20393  lmhmlsp  20394  lmhmkerlss  20396  reslmhm  20397  islmim  20407  lmicrcl  20416  lindfmm  21117  lindsmm  21118  lmhmclm  24333  lmhmlvec2  31842  dimkerim  31848  lmhmlvec  40477  lmhmfgima  41126  lnmepi  41127  lmhmfgsplit  41128  lmhmlnmsplit  41129