Theorem lmodfgrp 20623

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  ‘cfv 6542  Scalarcsca 17204  Grpcgrp 18855  Ringcrg 20127  LModclmod 20614

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rab 3431  df-v 3474  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 6494  df-fv 6550  df-ov 7414  df-ring 20129  df-lmod 20616

This theorem is referenced by:  lmodacl  20626  lmodsn0  20628  lmodvneg1  20659  lssvsubcl  20698  lspsnneg  20761  lvecvscan2  20870  lspexch  20887  lspsolvlem  20900  ipsubdir  21414  ipsubdi  21415  ip2eq  21425  ocvlss  21444  lsmcss  21464  islindf4  21612  ascl0  21657  clmfgrp  24818  lmodvslmhm  32472  lflmul  38241  lkrlss  38268  eqlkr  38272  lkrlsp  38275  lshpkrlem1  38283  ldualvsubval  38330  lcfrlem1  40716  lcdvsubval  40792  lmodvsmdi  47146  lincsum  47197  lincsumcl  47199  lincext1  47222  lindslinindsimp1  47225  lindslinindimp2lem1  47226  lindslinindsimp2lem5  47230  ldepsprlem  47240  ldepspr  47241  lincresunit3lem3  47242  lincresunit3lem1  47247  lincresunit3lem2  47248  lincresunit3  47249