Theorem lmodfgrp 20831

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6536  Scalarcsca 17279  Grpcgrp 18921  Ringcrg 20198  LModclmod 20822

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 2708  ax-nul 5281

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 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rab 3421  df-v 3466  df-sbc 3771  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-ring 20200  df-lmod 20824

This theorem is referenced by:  lmodacl  20834  lmodsn0  20836  lmodvneg1  20867  lssvsubcl  20906  lspsnneg  20968  lvecvscan2  21078  lspexch  21095  lspsolvlem  21108  ipsubdir  21607  ipsubdi  21608  ip2eq  21618  ocvlss  21637  lsmcss  21657  islindf4  21803  ascl0  21849  clmfgrp  25027  lmodvslmhm  33049  lflmul  39091  lkrlss  39118  eqlkr  39122  lkrlsp  39125  lshpkrlem1  39133  ldualvsubval  39180  lcfrlem1  41566  lcdvsubval  41642  lmodvsmdi  48321  lincsum  48372  lincsumcl  48374  lincext1  48397  lindslinindsimp1  48400  lindslinindimp2lem1  48401  lindslinindsimp2lem5  48405  ldepsprlem  48415  ldepspr  48416  lincresunit3lem3  48417  lincresunit3lem1  48422  lincresunit3lem2  48423  lincresunit3  48424