Theorem lmodfgrp 20855

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6492  Scalarcsca 17214  Grpcgrp 18900  Ringcrg 20205  LModclmod 20846

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 2709  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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-ring 20207  df-lmod 20848

This theorem is referenced by:  lmodacl  20858  lmodsn0  20860  lmodvneg1  20891  lssvsubcl  20930  lspsnneg  20992  lvecvscan2  21102  lspexch  21119  lspsolvlem  21132  ipsubdir  21632  ipsubdi  21633  ip2eq  21643  ocvlss  21662  lsmcss  21682  islindf4  21828  ascl0  21874  clmfgrp  25048  lmodvslmhm  33126  lflmul  39528  lkrlss  39555  eqlkr  39559  lkrlsp  39562  lshpkrlem1  39570  ldualvsubval  39617  lcfrlem1  42002  lcdvsubval  42078  lmodvsmdi  48867  lincsum  48917  lincsumcl  48919  lincext1  48942  lindslinindsimp1  48945  lindslinindimp2lem1  48946  lindslinindsimp2lem5  48950  ldepsprlem  48960  ldepspr  48961  lincresunit3lem3  48962  lincresunit3lem1  48967  lincresunit3lem2  48968  lincresunit3  48969