Theorem lmodfgrp 21149

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ‘cfv 6538  Scalarcsca 17436  Grpcgrp 19149  Ringcrg 20464  LModclmod 21140

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-ring 20466  df-lmod 21142

This theorem is used by:  lmodacl  21152  lmodsn0  21154  lmodvneg1  21185  lssvsubcl  21224  lspsnneg  21286  lvecvscan2  21395  lspexch  21412  lspsolvlem  21425  ipsubdir  21953  ipsubdi  21954  ip2eq  21964  ocvlss  21983  lsmcss  22003  islindf4  22149  ascl0  22197  clmfgrp  25397  lmodvslmhm  33657  lflmul  40218  lkrlss  40245  eqlkr  40249  lkrlsp  40252  lshpkrlem1  40260  ldualvsubval  40307  lcfrlem1  42692  lcdvsubval  42768  lmodvsmdi  49584  lincsum  49634  lincsumcl  49636  lincext1  49659  lindslinindsimp1  49662  lindslinindimp2lem1  49663  lindslinindsimp2lem5  49667  ldepsprlem  49677  ldepspr  49678  lincresunit3lem3  49679  lincresunit3lem1  49684  lincresunit3lem2  49685  lincresunit3  49686