Theorem lmodfgrp 20782

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  Scalarcsca 17230  Grpcgrp 18872  Ringcrg 20149  LModclmod 20773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-ring 20151  df-lmod 20775

This theorem is referenced by:  lmodacl  20785  lmodsn0  20787  lmodvneg1  20818  lssvsubcl  20857  lspsnneg  20919  lvecvscan2  21029  lspexch  21046  lspsolvlem  21059  ipsubdir  21558  ipsubdi  21559  ip2eq  21569  ocvlss  21588  lsmcss  21608  islindf4  21754  ascl0  21800  clmfgrp  24978  lmodvslmhm  32997  lflmul  39068  lkrlss  39095  eqlkr  39099  lkrlsp  39102  lshpkrlem1  39110  ldualvsubval  39157  lcfrlem1  41543  lcdvsubval  41619  lmodvsmdi  48371  lincsum  48422  lincsumcl  48424  lincext1  48447  lindslinindsimp1  48450  lindslinindimp2lem1  48451  lindslinindsimp2lem5  48455  ldepsprlem  48465  ldepspr  48466  lincresunit3lem3  48467  lincresunit3lem1  48472  lincresunit3lem2  48473  lincresunit3  48474