Theorem lmodfgrp 20820

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ‘cfv 6492  Scalarcsca 17180  Grpcgrp 18863  Ringcrg 20168  LModclmod 20811

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-ring 20170  df-lmod 20813

This theorem is referenced by:  lmodacl  20823  lmodsn0  20825  lmodvneg1  20856  lssvsubcl  20895  lspsnneg  20957  lvecvscan2  21067  lspexch  21084  lspsolvlem  21097  ipsubdir  21597  ipsubdi  21598  ip2eq  21608  ocvlss  21627  lsmcss  21647  islindf4  21793  ascl0  21840  clmfgrp  25027  lmodvslmhm  33133  lflmul  39324  lkrlss  39351  eqlkr  39355  lkrlsp  39358  lshpkrlem1  39366  ldualvsubval  39413  lcfrlem1  41798  lcdvsubval  41874  lmodvsmdi  48621  lincsum  48671  lincsumcl  48673  lincext1  48696  lindslinindsimp1  48699  lindslinindimp2lem1  48700  lindslinindsimp2lem5  48704  ldepsprlem  48714  ldepspr  48715  lincresunit3lem3  48716  lincresunit3lem1  48721  lincresunit3lem2  48722  lincresunit3  48723