Theorem lmodfgrp 20868

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  ‘cfv 6560  Scalarcsca 17301  Grpcgrp 18952  Ringcrg 20231  LModclmod 20859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-nul 5305

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rab 3436  df-v 3481  df-sbc 3788  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435  df-ring 20233  df-lmod 20861

This theorem is referenced by:  lmodacl  20871  lmodsn0  20873  lmodvneg1  20904  lssvsubcl  20943  lspsnneg  21005  lvecvscan2  21115  lspexch  21132  lspsolvlem  21145  ipsubdir  21661  ipsubdi  21662  ip2eq  21672  ocvlss  21691  lsmcss  21711  islindf4  21859  ascl0  21905  clmfgrp  25105  lmodvslmhm  33054  lflmul  39070  lkrlss  39097  eqlkr  39101  lkrlsp  39104  lshpkrlem1  39112  ldualvsubval  39159  lcfrlem1  41545  lcdvsubval  41621  lmodvsmdi  48300  lincsum  48351  lincsumcl  48353  lincext1  48376  lindslinindsimp1  48379  lindslinindimp2lem1  48380  lindslinindsimp2lem5  48384  ldepsprlem  48394  ldepspr  48395  lincresunit3lem3  48396  lincresunit3lem1  48401  lincresunit3lem2  48402  lincresunit3  48403