Theorem lmodfgrp 20624

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  ‘cfv 6543  Scalarcsca 17205  Grpcgrp 18856  Ringcrg 20128  LModclmod 20615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rab 3432  df-v 3475  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7415  df-ring 20130  df-lmod 20617

This theorem is referenced by:  lmodacl  20627  lmodsn0  20629  lmodvneg1  20660  lssvsubcl  20699  lspsnneg  20762  lvecvscan2  20871  lspexch  20888  lspsolvlem  20901  ipsubdir  21415  ipsubdi  21416  ip2eq  21426  ocvlss  21445  lsmcss  21465  islindf4  21613  ascl0  21658  clmfgrp  24819  lmodvslmhm  32473  lflmul  38242  lkrlss  38269  eqlkr  38273  lkrlsp  38276  lshpkrlem1  38284  ldualvsubval  38331  lcfrlem1  40717  lcdvsubval  40793  lmodvsmdi  47147  lincsum  47198  lincsumcl  47200  lincext1  47223  lindslinindsimp1  47226  lindslinindimp2lem1  47227  lindslinindsimp2lem5  47231  ldepsprlem  47241  ldepspr  47242  lincresunit3lem3  47243  lincresunit3lem1  47248  lincresunit3lem2  47249  lincresunit3  47250