Theorem lmodfgrp 21059

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  Scalarcsca 17351  Grpcgrp 19063  Ringcrg 20378  LModclmod 21050

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 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-ring 20380  df-lmod 21052

This theorem is used by:  lmodacl  21062  lmodsn0  21064  lmodvneg1  21095  lssvsubcl  21134  lspsnneg  21196  lvecvscan2  21305  lspexch  21322  lspsolvlem  21335  ipsubdir  21861  ipsubdi  21862  ip2eq  21872  ocvlss  21891  lsmcss  21911  islindf4  22057  ascl0  22105  clmfgrp  25305  lmodvslmhm  33498  lflmul  39949  lkrlss  39976  eqlkr  39980  lkrlsp  39983  lshpkrlem1  39991  ldualvsubval  40038  lcfrlem1  42423  lcdvsubval  42499  lmodvsmdi  49317  lincsum  49367  lincsumcl  49369  lincext1  49392  lindslinindsimp1  49395  lindslinindimp2lem1  49396  lindslinindsimp2lem5  49400  ldepsprlem  49410  ldepspr  49411  lincresunit3lem3  49412  lincresunit3lem1  49417  lincresunit3lem2  49418  lincresunit3  49419