Theorem lmodfgrp 20804

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ‘cfv 6486  Scalarcsca 17166  Grpcgrp 18848  Ringcrg 20153  LModclmod 20795

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 2115  ax-9 2123  ax-ext 2705  ax-nul 5246

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 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-ring 20155  df-lmod 20797

This theorem is referenced by:  lmodacl  20807  lmodsn0  20809  lmodvneg1  20840  lssvsubcl  20879  lspsnneg  20941  lvecvscan2  21051  lspexch  21068  lspsolvlem  21081  ipsubdir  21581  ipsubdi  21582  ip2eq  21592  ocvlss  21611  lsmcss  21631  islindf4  21777  ascl0  21823  clmfgrp  24999  lmodvslmhm  33037  lflmul  39187  lkrlss  39214  eqlkr  39218  lkrlsp  39221  lshpkrlem1  39229  ldualvsubval  39276  lcfrlem1  41661  lcdvsubval  41737  lmodvsmdi  48503  lincsum  48554  lincsumcl  48556  lincext1  48579  lindslinindsimp1  48582  lindslinindimp2lem1  48583  lindslinindsimp2lem5  48587  ldepsprlem  48597  ldepspr  48598  lincresunit3lem3  48599  lincresunit3lem1  48604  lincresunit3lem2  48605  lincresunit3  48606