Theorem lmodfgrp 20472

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ‘cfv 6540  Scalarcsca 17196  Grpcgrp 18815  Ringcrg 20049  LModclmod 20463

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rab 3433  df-v 3476  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-ring 20051  df-lmod 20465

This theorem is referenced by:  lmodacl  20475  lmodsn0  20477  lmodvneg1  20507  lssvsubcl  20546  lspsnneg  20609  lvecvscan2  20717  lspexch  20734  lspsolvlem  20747  ipsubdir  21186  ipsubdi  21187  ip2eq  21197  ocvlss  21216  lsmcss  21236  islindf4  21384  ascl0  21429  clmfgrp  24578  lmodvslmhm  32189  lflmul  37926  lkrlss  37953  eqlkr  37957  lkrlsp  37960  lshpkrlem1  37968  ldualvsubval  38015  lcfrlem1  40401  lcdvsubval  40477  lmodvsmdi  47011  lincsum  47063  lincsumcl  47065  lincext1  47088  lindslinindsimp1  47091  lindslinindimp2lem1  47092  lindslinindsimp2lem5  47096  ldepsprlem  47106  ldepspr  47107  lincresunit3lem3  47108  lincresunit3lem1  47113  lincresunit3lem2  47114  lincresunit3  47115