lmodfgrp - Metamath Proof Explorer

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

Theorem lmodfgrp 19908

Description: The scalar component of a left module is an additive group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)

**Hypothesis**
Ref	Expression
lmodring.1	⊢ 𝐹 = (Scalar‘𝑊)

**Assertion**
Ref	Expression
lmodfgrp	⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp)

**Proof of Theorem lmodfgrp**
Step	Hyp	Ref	Expression
1		lmodring.1	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
2	1	lmodring 19907	. 2 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)
3		ringgrp 19567	. 2 ⊢ (𝐹 ∈ Ring → 𝐹 ∈ Grp)
4	2, 3	syl 17	1 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1543 ∈ wcel 2110 ‘cfv 6380 Scalarcsca 16805 Grpcgrp 18365 Ringcrg 19562 LModclmod 19899

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-nul 5199

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3410 df-sbc 3695 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-uni 4820 df-br 5054 df-iota 6338 df-fv 6388 df-ov 7216 df-ring 19564 df-lmod 19901

This theorem is referenced by: lmodacl 19910 lmodsn0 19912 lmodvneg1 19942 lssvsubcl 19980 lspsnneg 20043 lvecvscan2 20149 lspexch 20166 lspsolvlem 20179 ipsubdir 20604 ipsubdi 20605 ip2eq 20615 ocvlss 20634 lsmcss 20654 islindf4 20800 ascl0 20843 clmfgrp 23968 lmodvslmhm 31029 lflmul 36819 lkrlss 36846 eqlkr 36850 lkrlsp 36853 lshpkrlem1 36861 ldualvsubval 36908 lcfrlem1 39293 lcdvsubval 39369 lmodvsmdi 45391 lincsum 45443 lincsumcl 45445 lincext1 45468 lindslinindsimp1 45471 lindslinindimp2lem1 45472 lindslinindsimp2lem5 45476 ldepsprlem 45486 ldepspr 45487 lincresunit3lem3 45488 lincresunit3lem1 45493 lincresunit3lem2 45494 lincresunit3 45495

W3C validator