Theorem lmodfgrp 18695

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  ‘cfv 5804  Scalarcsca 15771  Grpcgrp 17245  Ringcrg 18370  LModclmod 18686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-ring 18372  df-lmod 18688

This theorem is referenced by:  lmodacl  18697  lmodsn0  18699  lmodvneg1  18729  lssvsubcl  18765  lspsnneg  18827  lvecvscan2  18933  lspexch  18950  lspsolvlem  18963  ipsubdir  19806  ipsubdi  19807  ip2eq  19817  ocvlss  19835  lsmcss  19855  islindf4  19996  clmfgrp  22679  lflmul  33373  lkrlss  33400  eqlkr  33404  lkrlsp  33407  lshpkrlem1  33415  ldualvsubval  33462  lcfrlem1  35849  lcdvsubval  35925  lmodvsmdi  41957  ascl0  41959  lincsum  42012  lincsumcl  42014  lincext1  42037  lindslinindsimp1  42040  lindslinindimp2lem1  42041  lindslinindsimp2lem5  42045  ldepsprlem  42055  ldepspr  42056  lincresunit3lem3  42057  lincresunit3lem1  42062  lincresunit3lem2  42063  lincresunit3  42064