Theorem lmodfgrp 20884

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  ‘cfv 6563  Scalarcsca 17301  Grpcgrp 18964  Ringcrg 20251  LModclmod 20875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-nul 5312

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rab 3434  df-v 3480  df-sbc 3792  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-ring 20253  df-lmod 20877

This theorem is referenced by:  lmodacl  20887  lmodsn0  20889  lmodvneg1  20920  lssvsubcl  20960  lspsnneg  21022  lvecvscan2  21132  lspexch  21149  lspsolvlem  21162  ipsubdir  21678  ipsubdi  21679  ip2eq  21689  ocvlss  21708  lsmcss  21728  islindf4  21876  ascl0  21922  clmfgrp  25118  lmodvslmhm  33036  lflmul  39050  lkrlss  39077  eqlkr  39081  lkrlsp  39084  lshpkrlem1  39092  ldualvsubval  39139  lcfrlem1  41525  lcdvsubval  41601  lmodvsmdi  48224  lincsum  48275  lincsumcl  48277  lincext1  48300  lindslinindsimp1  48303  lindslinindimp2lem1  48304  lindslinindsimp2lem5  48308  ldepsprlem  48318  ldepspr  48319  lincresunit3lem3  48320  lincresunit3lem1  48325  lincresunit3lem2  48326  lincresunit3  48327