Theorem lmodfgrp 21027

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  ‘cfv 6543  Scalarcsca 17338  Grpcgrp 19031  Ringcrg 20346  LModclmod 21018

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-ring 20348  df-lmod 21020

This theorem is used by:  lmodacl  21030  lmodsn0  21032  lmodvneg1  21063  lssvsubcl  21102  lspsnneg  21164  lvecvscan2  21273  lspexch  21290  lspsolvlem  21303  ipsubdir  21829  ipsubdi  21830  ip2eq  21840  ocvlss  21859  lsmcss  21879  islindf4  22025  ascl0  22071  clmfgrp  25267  lmodvslmhm  33401  lflmul  39883  lkrlss  39910  eqlkr  39914  lkrlsp  39917  lshpkrlem1  39925  ldualvsubval  39972  lcfrlem1  42357  lcdvsubval  42433  lmodvsmdi  49200  lincsum  49250  lincsumcl  49252  lincext1  49275  lindslinindsimp1  49278  lindslinindimp2lem1  49279  lindslinindsimp2lem5  49283  ldepsprlem  49293  ldepspr  49294  lincresunit3lem3  49295  lincresunit3lem1  49300  lincresunit3lem2  49301  lincresunit3  49302