Theorem lmodfgrp 20971

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ‘cfv 6538  Scalarcsca 17314  Grpcgrp 19001  Ringcrg 20316  LModclmod 20962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-ring 20318  df-lmod 20964

This theorem is referenced by:  lmodacl  20974  lmodsn0  20976  lmodvneg1  21007  lssvsubcl  21046  lspsnneg  21108  lvecvscan2  21217  lspexch  21234  lspsolvlem  21247  ipsubdir  21773  ipsubdi  21774  ip2eq  21784  ocvlss  21803  lsmcss  21823  islindf4  21969  ascl0  22015  clmfgrp  25211  lmodvslmhm  33348  lflmul  39820  lkrlss  39847  eqlkr  39851  lkrlsp  39854  lshpkrlem1  39862  ldualvsubval  39909  lcfrlem1  42294  lcdvsubval  42370  lmodvsmdi  49136  lincsum  49186  lincsumcl  49188  lincext1  49211  lindslinindsimp1  49214  lindslinindimp2lem1  49215  lindslinindsimp2lem5  49219  ldepsprlem  49229  ldepspr  49230  lincresunit3lem3  49231  lincresunit3lem1  49236  lincresunit3lem2  49237  lincresunit3  49238