Theorem lmodfgrp 20790

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6486  Scalarcsca 17182  Grpcgrp 18830  Ringcrg 20136  LModclmod 20781

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 2701  ax-nul 5248

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-ring 20138  df-lmod 20783

This theorem is referenced by:  lmodacl  20793  lmodsn0  20795  lmodvneg1  20826  lssvsubcl  20865  lspsnneg  20927  lvecvscan2  21037  lspexch  21054  lspsolvlem  21067  ipsubdir  21567  ipsubdi  21568  ip2eq  21578  ocvlss  21597  lsmcss  21617  islindf4  21763  ascl0  21809  clmfgrp  24987  lmodvslmhm  33016  lflmul  39046  lkrlss  39073  eqlkr  39077  lkrlsp  39080  lshpkrlem1  39088  ldualvsubval  39135  lcfrlem1  41521  lcdvsubval  41597  lmodvsmdi  48364  lincsum  48415  lincsumcl  48417  lincext1  48440  lindslinindsimp1  48443  lindslinindimp2lem1  48444  lindslinindsimp2lem5  48448  ldepsprlem  48458  ldepspr  48459  lincresunit3lem3  48460  lincresunit3lem1  48465  lincresunit3lem2  48466  lincresunit3  48467