Theorem lmodfgrp 20800

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  ‘cfv 6481  Scalarcsca 17161  Grpcgrp 18843  Ringcrg 20149  LModclmod 20791

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-ring 20151  df-lmod 20793

This theorem is referenced by:  lmodacl  20803  lmodsn0  20805  lmodvneg1  20836  lssvsubcl  20875  lspsnneg  20937  lvecvscan2  21047  lspexch  21064  lspsolvlem  21077  ipsubdir  21577  ipsubdi  21578  ip2eq  21588  ocvlss  21607  lsmcss  21627  islindf4  21773  ascl0  21819  clmfgrp  24996  lmodvslmhm  33025  lflmul  39106  lkrlss  39133  eqlkr  39137  lkrlsp  39140  lshpkrlem1  39148  ldualvsubval  39195  lcfrlem1  41580  lcdvsubval  41656  lmodvsmdi  48409  lincsum  48460  lincsumcl  48462  lincext1  48485  lindslinindsimp1  48488  lindslinindimp2lem1  48489  lindslinindsimp2lem5  48493  ldepsprlem  48503  ldepspr  48504  lincresunit3lem3  48505  lincresunit3lem1  48510  lincresunit3lem2  48511  lincresunit3  48512