lmghm - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lmghm		Structured version Visualization version GIF version

Theorem lmghm 19356

Description: A homomorphism of left modules is a homomorphism of groups. (Contributed by Stefan O'Rear, 1-Jan-2015.)

**Assertion**
Ref	Expression
lmghm	⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))

**Proof of Theorem lmghm**
Step	Hyp	Ref	Expression
1		eqid 2803	. . 3 ⊢ (Scalar‘𝑆) = (Scalar‘𝑆)
2		eqid 2803	. . 3 ⊢ (Scalar‘𝑇) = (Scalar‘𝑇)
3	1, 2	lmhmlem 19354	. 2 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → ((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (Scalar‘𝑇) = (Scalar‘𝑆))))
4		simprl 788	. 2 ⊢ (((𝑆 ∈ LMod ∧ 𝑇 ∈ LMod) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (Scalar‘𝑇) = (Scalar‘𝑆))) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
5	3, 4	syl 17	1 ⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 ‘cfv 6105 (class class class)co 6882 Scalarcsca 16274 GrpHom cghm 17974 LModclmod 19185 LMHom clmhm 19344

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2379 ax-ext 2781 ax-sep 4979 ax-nul 4987 ax-pow 5039 ax-pr 5101

This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2593 df-eu 2611 df-clab 2790 df-cleq 2796 df-clel 2799 df-nfc 2934 df-ral 3098 df-rex 3099 df-rab 3102 df-v 3391 df-sbc 3638 df-dif 3776 df-un 3778 df-in 3780 df-ss 3787 df-nul 4120 df-if 4282 df-sn 4373 df-pr 4375 df-op 4379 df-uni 4633 df-br 4848 df-opab 4910 df-id 5224 df-xp 5322 df-rel 5323 df-cnv 5324 df-co 5325 df-dm 5326 df-iota 6068 df-fun 6107 df-fv 6113 df-ov 6885 df-oprab 6886 df-mpt2 6887 df-lmhm 19347

This theorem is referenced by: lmhmf 19359 islmhm2 19363 lmhmco 19368 lmhmplusg 19369 lmhmvsca 19370 lmhmf1o 19371 lmhmima 19372 lmhmpreima 19373 reslmhm 19377 reslmhm2 19378 reslmhm2b 19379 lmhmeql 19380 lmimgim 19390 ip0l 20309 ipdir 20312 islindf5 20507 isnmhm2 22888 nmoleub2lem 23245 nmoleub2lem2 23247 nmhmcn 23251 kercvrlsm 38442 pwssplit4 38448 mendring 38551

W3C validator