Theorem lmodfgrp 20864

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 20863	. 2 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)
3		ringgrp 20219	. 2 ⊢ (𝐹 ∈ Ring → 𝐹 ∈ Grp)
4	2, 3	syl 17	1 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Grp)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6498  Scalarcsca 17223  Grpcgrp 18909  Ringcrg 20214  LModclmod 20855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-ring 20216  df-lmod 20857

This theorem is referenced by:  lmodacl  20867  lmodsn0  20869  lmodvneg1  20900  lssvsubcl  20939  lspsnneg  21001  lvecvscan2  21110  lspexch  21127  lspsolvlem  21140  ipsubdir  21622  ipsubdi  21623  ip2eq  21633  ocvlss  21652  lsmcss  21672  islindf4  21818  ascl0  21864  clmfgrp  25038  lmodvslmhm  33111  lflmul  39514  lkrlss  39541  eqlkr  39545  lkrlsp  39548  lshpkrlem1  39556  ldualvsubval  39603  lcfrlem1  41988  lcdvsubval  42064  lmodvsmdi  48855  lincsum  48905  lincsumcl  48907  lincext1  48930  lindslinindsimp1  48933  lindslinindimp2lem1  48934  lindslinindsimp2lem5  48938  ldepsprlem  48948  ldepspr  48949  lincresunit3lem3  48950  lincresunit3lem1  48955  lincresunit3lem2  48956  lincresunit3  48957